Theorem neg_in_imp_reverse_elim ≪ | index | src | ≫

→中¬逆消除

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

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

Axiom use

ZFC (ax_p3)