Theorem bieq2d ≪ | index | src | ≫

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

a -> (b <-> b)

a -> (c <-> d)

a -> (b <-> c <-> (b <-> d))

Axiom use