Theorem aneq1i | index | src |

theorem aneq1i (a b c: wff): $ a <-> b $ > $ a /\ c <-> b /\ c $;
StepHypRefExpression
1 id
(a <-> b) -> (a <-> b)
2 1 aneq1d
(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)