Theorem wff_iff_false_iff_negself ≪ | index | src | ≫

\iff真值表：(A \iff \false) \iff \neg A

theorem wff_iff_false_iff_negself (A: wff): $ (A \iff \false) \iff \neg A $;

Step	Hyp	Ref	Expression
1		iff_symm	(\neg A \iff A \iff \false) \imp ((A \iff \false) \iff \neg A)
2		assign_false	\neg A \iff A \iff \false
3	1, 2	ax_mp	(A \iff \false) \iff \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)