Theorem imp_right_neg_permute ≪ | index | src | ≫

→右¬置换

theorem imp_right_neg_permute (A B: wff):
  $ (A \imp \neg B) \imp B \imp \neg A $;
StepHypRefExpression
1 imp_for_imp_right_reverse_intro 
((A \imp \neg B) \imp \neg \neg A \imp \neg B) \imp ((\neg \neg A \imp \neg B) \imp B \imp \neg A) \imp (A \imp \neg B) \imp B \imp \neg A
2 imp_for_imp_right_reverse_intro 
(\neg \neg A \imp A) \imp (A \imp \neg B) \imp \neg \neg A \imp \neg B
3 neg_neg_elim 
\neg \neg A \imp A
4 2, 3 mp 
(A \imp \neg B) \imp \neg \neg A \imp \neg B
5 1, 4 mp 
((\neg \neg A \imp \neg B) \imp B \imp \neg A) \imp (A \imp \neg B) \imp B \imp \neg A
6 neg_in_imp_reverse_elim 
(\neg \neg A \imp \neg B) \imp B \imp \neg A
7 5, 6 mp 
(A \imp \neg B) \imp B \imp \neg A

Axiom use

ZFC (ax_mp, ax_p1, ax_p2, ax_p3)