Theorem negneg_intro ≪ | index | src | ≫

\neg\neg引出

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

Step	Hyp	Ref	Expression
1		neg_imp_elimrev	(\neg \neg \neg A \imp \neg A) \imp A \imp \neg \neg A
2		negneg_elim	\neg \neg \neg A \imp \neg A
3	1, 2	ax_mp	A \imp \neg \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)