Theorem imp_allocrev_neg ≪ | index | src | ≫

\imp逆指配\neg

theorem imp_allocrev_neg (A B: wff): $ A \imp B \iff \neg B \imp \neg A $;
StepHypRefExpression
1 iff_comp 
((A \imp B) \imp \neg B \imp \neg A) \imp ((\neg B \imp \neg A) \imp A \imp B) \imp (A \imp B \iff \neg B \imp \neg A)
2 imp_introrev_neg 
(A \imp B) \imp \neg B \imp \neg A
3 1, 2 ax_mp 
((\neg B \imp \neg A) \imp A \imp B) \imp (A \imp B \iff \neg B \imp \neg A)
4 neg_imp_elimrev 
(\neg B \imp \neg A) \imp A \imp B
5 3, 4 ax_mp 
A \imp B \iff \neg B \imp \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)