Theorem bieqd ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		hyp h1	a -> (b <-> c)
2		hyp h2	a -> (d <-> e)
3	1, 2	imeqd	a -> (b -> d <-> c -> e)
4	2, 1	imeqd	a -> (d -> b <-> e -> c)
5	3, 4	aneqd	a -> ((b -> d) /\ (d -> b) <-> (c -> e) /\ (e -> c))
6	5	conv iff	a -> (b <-> d <-> (c <-> e))

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)