Theorem imeq1i | index | src |

theorem imeq1i (a b c: wff): $ a <-> b $ > $ a -> c <-> b -> c $;
StepHypRefExpression
1 id
(a <-> b) -> (a <-> b)
2 1 imeq1d
(a <-> b) -> (a -> c <-> b -> c)
3 hyp h
a <-> b
4 2, 3 ax_mp
a -> c <-> b -> c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)