Theorem mtoi 654

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 653	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  664  mtbiri  665  pwnss  4091  nsuceq0g  4348  abnex  4376  reg2exmidlema  4457  ordsuc  4486  onnmin  4491  ssnel  4492  ordtri2or2exmid  4494  reg3exmidlemwe  4501  acexmidlemab  5776  reldmtpos  6158  dmtpos  6161  2pwuninelg  6188  onunsnss  6813  snon0  6832  exmidomni  7022  pr2ne  7065  ltexprlemdisj  7438  recexprlemdisj  7462  caucvgprlemnkj  7498  caucvgprprlemnkltj  7521  caucvgprprlemnkeqj  7522  caucvgprprlemnjltk  7523  inelr  8370  rimul  8371  recgt0  8632  zfz1iso  10616  isprm2  11834  nprmdvds1  11856  divgcdodd  11857  coprm  11858  coseq0q4123  12963  pwle2  13366  exmid1stab  13368  nninfalllem1  13378  nninfall  13379  nninfsellemqall  13386