Theorem negneg_alloc ≪ | index | src | ≫

\neg\neg等价

theorem negneg_alloc (A: wff): $ A \iff \neg \neg A $;


(A \imp \neg \neg A) \imp (\neg \neg A \imp A) \imp (A \iff \neg \neg A)
A \imp \neg \neg A
(\neg \neg A \imp A) \imp (A \iff \neg \neg A)
\neg \neg A \imp A
A \iff \neg \neg A

Step	Hyp	Ref	Expression
1		iff_comp	(A \imp \neg \neg A) \imp (\neg \neg A \imp A) \imp (A \iff \neg \neg A)
2		negneg_intro	A \imp \neg \neg A
3	1, 2	ax_mp	(\neg \neg A \imp A) \imp (A \iff \neg \neg A)
4		negneg_elim	\neg \neg A \imp A
5	3, 4	ax_mp	A \iff \neg \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)