Theorem imp_neg_swap ≪ | index | src | ≫

\imp\neg交换

theorem imp_neg_swap (A B: wff): $ (A \imp \neg B) \imp B \imp \neg A $;
StepHypRefExpression
1 imp_introrevr_imp 
((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_introrevr_imp 
(\neg \neg A \imp A) \imp (A \imp \neg B) \imp \neg \neg A \imp \neg B
3 negneg_elim 
\neg \neg A \imp A
4 2, 3 ax_mp 
(A \imp \neg B) \imp \neg \neg A \imp \neg B
5 1, 4 ax_mp 
((\neg \neg A \imp \neg B) \imp B \imp \neg A) \imp (A \imp \neg B) \imp B \imp \neg A
6 neg_imp_elimrev 
(\neg \neg A \imp \neg B) \imp B \imp \neg A
7 5, 6 ax_mp 
(A \imp \neg B) \imp B \imp \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)