Theorem imp_left_neg_imp_same ≪ | index | src | ≫

→左¬自蕴

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

Axiom use

ZFC (ax_mp, ax_p1, ax_p2, ax_p3)