Theorem neg_imp_elimrev ≪ | index | src | ≫

\neg\imp逆消除

theorem neg_imp_elimrev (A B: wff): $ (\neg A \imp \neg B) \imp B \imp A $;

Step	Hyp	Ref	Expression
1		ax_3	(\neg A \imp \neg B) \imp B \imp A

Axiom use

Logic (ax_3)