Theorem bitr4g | index | src |

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

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)