Theorem wff_imp_true_iff_true ≪ | index | src | ≫

\imp真值表：wff \imp \true \iff \true

theorem wff_imp_true_iff_true (A: wff): $ A \imp \true \iff \true $;

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)