Theorem imp_neg_tosame_neg ≪ | index | src | ≫

\imp\neg推出同一\neg

theorem imp_neg_tosame_neg (A: wff): $ (A \imp \neg A) \imp \neg A $;
StepHypRefExpression
1 imp_tran 
((A \imp \neg A) \imp \neg \neg A \imp \neg A) \imp ((\neg \neg A \imp \neg A) \imp \neg A) \imp (A \imp \neg A) \imp \neg A
2 imp_introrev_neg 
(A \imp \neg A) \imp \neg \neg A \imp \neg A
3 1, 2 ax_mp 
((\neg \neg A \imp \neg A) \imp \neg A) \imp (A \imp \neg A) \imp \neg A
4 neg_imp_tosame 
(\neg \neg A \imp \neg A) \imp \neg A
5 3, 4 ax_mp 
(A \imp \neg A) \imp \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)