Theorem imp_right_neg_imp_neg_same ≪ | index | src | ≫

→右¬蕴否

theorem imp_right_neg_imp_neg_same (A: wff): $ (A \imp \neg A) \imp \neg A $;
StepHypRefExpression
1 imp_trans_curried 
((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 neg_in_imp_reverse_intro 
(A \imp \neg A) \imp \neg \neg A \imp \neg A
3 1, 2 mp 
((\neg \neg A \imp \neg A) \imp \neg A) \imp (A \imp \neg A) \imp \neg A
4 imp_left_neg_imp_same 
(\neg \neg A \imp \neg A) \imp \neg A
5 3, 4 mp 
(A \imp \neg A) \imp \neg A

Axiom use

ZFC (ax_mp, ax_p1, ax_p2, ax_p3)