Theorem neg_neg_intro ≪ | index | src | ≫

¬¬引出

theorem neg_neg_intro (A: wff): $ A \imp \neg \neg A $;

Step	Hyp	Ref	Expression
1		neg_in_imp_reverse_elim	(\neg \neg \neg A \imp \neg A) \imp A \imp \neg \neg A
2		neg_neg_elim	\neg \neg \neg A \imp \neg A
3	1, 2	mp	A \imp \neg \neg A

Axiom use

ZFC (ax_mp, ax_p1, ax_p2, ax_p3)