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  4214  exmid1stab  4263  nsuceq0g  4478  abnex  4507  reg2exmidlema  4595  ordsuc  4624  onnmin  4629  ssnel  4630  ordtri2or2exmid  4632  ontri2orexmidim  4633  reg3exmidlemwe  4640  acexmidlemab  5956  reldmtpos  6357  dmtpos  6360  2pwuninelg  6387  onunsnss  7035  snon0  7058  nninfisol  7256  exmidomni  7265  pr2ne  7321  ltexprlemdisj  7749  recexprlemdisj  7773  caucvgprlemnkj  7809  caucvgprprlemnkltj  7832  caucvgprprlemnkeqj  7833  caucvgprprlemnjltk  7834  inelr  8687  rimul  8688  recgt0  8953  zfz1iso  11018  isprm2  12524  nprmdvds1  12547  divgcdodd  12550  coprm  12551  coseq0q4123  15391  lgsquad2lem2  15644  umgrislfupgrenlem  15806  lfgrnloopen  15809  pwle2  16107  nninfalllem1  16117  nninfall  16118  nninfsellemqall  16124