Theorem neg_neg_elim ≪ | index | src | ≫

¬¬消除

theorem neg_neg_elim (A: wff): $ \neg \neg A \imp A $;
StepHypRefExpression
1 imp_for_imp_left_insert 
(\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_trans_curried 
(\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_elim_with_imp 
\neg \neg A \imp \neg A \imp \neg \neg \neg A
4 2, 3 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_in_imp_reverse_elim 
(\neg A \imp \neg \neg \neg A) \imp \neg \neg A \imp A
6 4, 5 mp 
\neg \neg A \imp \neg \neg A \imp A
7 1, 6 mp 
(\neg \neg A \imp \neg \neg A) \imp \neg \neg A \imp A
8 imp_reflect 
\neg \neg A \imp \neg \neg A
9 7, 8 mp 
\neg \neg A \imp A

Axiom use

ZFC (ax_mp, ax_p1, ax_p2, ax_p3)