Theorem wff_imp_false_iff_neg_wff ≪ | index | src | ≫

\imp真值表：wff \imp \false \iff \neg wff

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

Step	Hyp	Ref	Expression
1		impfalse_eqv_negself	A \imp \false \iff \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)