Theorem mtoi 666

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  676  mtbiri  677  pwnss  4203  exmid1stab  4252  nsuceq0g  4465  abnex  4494  reg2exmidlema  4582  ordsuc  4611  onnmin  4616  ssnel  4617  ordtri2or2exmid  4619  ontri2orexmidim  4620  reg3exmidlemwe  4627  acexmidlemab  5938  reldmtpos  6339  dmtpos  6342  2pwuninelg  6369  onunsnss  7014  snon0  7037  nninfisol  7235  exmidomni  7244  pr2ne  7300  ltexprlemdisj  7719  recexprlemdisj  7743  caucvgprlemnkj  7779  caucvgprprlemnkltj  7802  caucvgprprlemnkeqj  7803  caucvgprprlemnjltk  7804  inelr  8657  rimul  8658  recgt0  8923  zfz1iso  10986  isprm2  12439  nprmdvds1  12462  divgcdodd  12465  coprm  12466  coseq0q4123  15306  lgsquad2lem2  15559  pwle2  15935  nninfalllem1  15945  nninfall  15946  nninfsellemqall  15952