Theorem syl5ibrcom | index | src |

theorem syl5ibrcom (a b c d: wff):
  $ c -> (b <-> d) $ >
  $ a -> d $ >
  $ a -> c -> b $;
StepHypRefExpression
1 hyp h2
a -> d
2 hyp h1
c -> (b <-> d)
3 2 bi2d
c -> d -> b
4 1, 3 syl5
c -> a -> b
5 4 com12
a -> c -> b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)