Theorem noteqi ≪ | index | src | ≫

theorem noteqi (a b: wff): $ a <-> b $ > $ ~a <-> ~b $;

Step	Hyp	Ref	Expression
1		noteq	(a <-> b) -> (~a <-> ~b)
2		hyp h	a <-> b
3	1, 2	ax_mp	~a <-> ~b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)