Theorem aneqd | index | src |

theorem aneqd (a b c d e: wff):
  $ a -> (b <-> c) $ >
  $ a -> (d <-> e) $ >
  $ a -> (b /\ d <-> c /\ e) $;
StepHypRefExpression
1 hyp h1
a -> (b <-> c)
2 1 bi1d
a -> b -> c
3 hyp h2
a -> (d <-> e)
4 3 bi1d
a -> d -> e
5 2, 4 animd
a -> b /\ d -> c /\ e
6 1 bi2d
a -> c -> b
7 3 bi2d
a -> e -> d
8 6, 7 animd
a -> c /\ e -> b /\ d
9 5, 8 ibid
a -> (b /\ d <-> c /\ e)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)