Theorem negneg_elim ≪ | index | src | ≫

\neg\neg消除

theorem negneg_elim (A: wff): $ \neg \neg A \imp A $;
StepHypRefExpression
1 imp_imp_insl 
(\neg \neg A \imp \neg \neg A \imp A) \imp (\neg \neg A \imp \neg \neg A) \imp \neg \neg A \imp A
2 imp_tran 
(\neg \neg A \imp \neg A \imp \neg \neg \neg A) \imp ((\neg A \imp \neg \neg \neg A) \imp \neg \neg A \imp A) \imp \neg \neg A \imp \neg \neg A \imp A
3 neg_elimintror_imp 
\neg \neg A \imp \neg A \imp \neg \neg \neg A
4 2, 3 ax_mp 
((\neg A \imp \neg \neg \neg A) \imp \neg \neg A \imp A) \imp \neg \neg A \imp \neg \neg A \imp A
5 neg_imp_elimrev 
(\neg A \imp \neg \neg \neg A) \imp \neg \neg A \imp A
6 4, 5 ax_mp 
\neg \neg A \imp \neg \neg A \imp A
7 1, 6 ax_mp 
(\neg \neg A \imp \neg \neg A) \imp \neg \neg A \imp A
8 imp_refl 
\neg \neg A \imp \neg \neg A
9 7, 8 ax_mp 
\neg \neg A \imp A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)