Theorem mtoi 668

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  678  mtbiri  679  pwnss  4242  exmid1stab  4291  nsuceq0g  4508  abnex  4537  reg2exmidlema  4625  ordsuc  4654  onnmin  4659  ssnel  4660  ordtri2or2exmid  4662  ontri2orexmidim  4663  reg3exmidlemwe  4670  acexmidlemab  5994  reldmtpos  6397  dmtpos  6400  2pwuninelg  6427  onunsnss  7075  snon0  7098  nninfisol  7296  exmidomni  7305  pr2ne  7361  ltexprlemdisj  7789  recexprlemdisj  7813  caucvgprlemnkj  7849  caucvgprprlemnkltj  7872  caucvgprprlemnkeqj  7873  caucvgprprlemnjltk  7874  inelr  8727  rimul  8728  recgt0  8993  zfz1iso  11058  isprm2  12634  nprmdvds1  12657  divgcdodd  12660  coprm  12661  coseq0q4123  15502  lgsquad2lem2  15755  umgrnloop0  15911  umgrislfupgrenlem  15922  lfgrnloopen  15925  pwle2  16323  nninfalllem1  16333  nninfall  16334  nninfsellemqall  16340