Theorem wff_iff_true_iff_self ≪ | index | src | ≫

\iff真值表：(A \iff \true) \iff A

theorem wff_iff_true_iff_self (A: wff): $ (A \iff \true) \iff A $;

Step	Hyp	Ref	Expression
1		iff_symm	(A \iff A \iff \true) \imp ((A \iff \true) \iff A)
2		assgin_true	A \iff A \iff \true
3	1, 2	ax_mp	(A \iff \true) \iff A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)