Theorem neg_imp_tosame ≪ | index | src | ≫

\neg\imp推出同一

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)