Theorem bitr3g | index | src |

theorem bitr3g (a b c d e: wff):
  $ b <-> d $ >
  $ c <-> e $ >
  $ a -> (b <-> c) $ >
  $ a -> (d <-> e) $;
StepHypRefExpression
1 bicom
(b <-> d) -> (d <-> b)
2 hyp h1
b <-> d
3 1, 2 ax_mp
d <-> b
4 hyp h2
c <-> e
5 hyp h
a -> (b <-> c)
6 4, 5 syl6bb
a -> (b <-> e)
7 3, 6 syl5bb
a -> (d <-> e)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)