Theorem bieq1d ≪ | index | src | ≫

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

a -> (b <-> c)

a -> (d <-> d)

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

Axiom use