Theorem iff_refl ≪ | index | src | ≫

\iff自反

theorem iff_refl (A: wff): $ A \iff A $;

Step	Hyp	Ref	Expression
1		iff_comp	(A \imp A) \imp (A \imp A) \imp (A \iff A)
2		imp_refl	A \imp A
3	1, 2	ax_mp	(A \imp A) \imp (A \iff A)
4	3, 2	ax_mp	A \iff A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)