Theorem true_imp_wff_iff_wff ≪ | index | src | ≫

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

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

Step	Hyp	Ref	Expression
1		trueimp_eqv_self	\true \imp A \iff A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)