Theorem bicom ≪ | index | src | ≫

theorem bicom (a b: wff): $ (a <-> b) -> (b <-> a) $;

(a <-> b) -> b -> a

(a <-> b) -> a -> b

(a <-> b) -> (b <-> a)

Axiom use