Theorem mtoi 664

Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)

Hypotheses

Ref	Expression
mtoi.1	⊢ ¬ 𝜒
mtoi.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mtoi	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtoi

Step	Hyp	Ref	Expression
1		mtoi.1	. . 3 ⊢ ¬ 𝜒
2	1	a1i 9	. 2 ⊢ (𝜑 → ¬ 𝜒)
3		mtoi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mtod 663	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 614  ax-in2 615

This theorem is referenced by:  mtbii  674  mtbiri  675  pwnss  4154  nsuceq0g  4412  abnex  4441  reg2exmidlema  4527  ordsuc  4556  onnmin  4561  ssnel  4562  ordtri2or2exmid  4564  ontri2orexmidim  4565  reg3exmidlemwe  4572  acexmidlemab  5859  reldmtpos  6244  dmtpos  6247  2pwuninelg  6274  onunsnss  6906  snon0  6925  nninfisol  7121  exmidomni  7130  pr2ne  7181  ltexprlemdisj  7580  recexprlemdisj  7604  caucvgprlemnkj  7640  caucvgprprlemnkltj  7663  caucvgprprlemnkeqj  7664  caucvgprprlemnjltk  7665  inelr  8515  rimul  8516  recgt0  8780  zfz1iso  10789  isprm2  12084  nprmdvds1  12107  divgcdodd  12110  coprm  12111  coseq0q4123  13835  pwle2  14317  exmid1stab  14319  nninfalllem1  14327  nninfall  14328  nninfsellemqall  14334