Theorem bicomd ≪ | index | src | ≫

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

(b <-> c) -> (c <-> b)

a -> (b <-> c)

a -> (c <-> b)

Axiom use