Theorem impbir ≪ | index | src | ≫

theorem impbir (a b c: wff): $ a -> (c <-> b) $ > $ a /\ b -> c $;

a -> (c <-> b)

a -> b -> c

a /\ b -> c

Axiom use