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  4243  exmid1stab  4292  nsuceq0g  4509  abnex  4538  reg2exmidlema  4626  ordsuc  4655  onnmin  4660  ssnel  4661  ordtri2or2exmid  4663  ontri2orexmidim  4664  reg3exmidlemwe  4671  acexmidlemab  6001  reldmtpos  6405  dmtpos  6408  2pwuninelg  6435  onunsnss  7090  snon0  7113  nninfisol  7311  exmidomni  7320  pr2ne  7376  ltexprlemdisj  7804  recexprlemdisj  7828  caucvgprlemnkj  7864  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnjltk  7889  inelr  8742  rimul  8743  recgt0  9008  zfz1iso  11076  isprm2  12654  nprmdvds1  12677  divgcdodd  12680  coprm  12681  coseq0q4123  15523  lgsquad2lem2  15776  umgrnloop0  15932  umgrislfupgrenlem  15943  lfgrnloopen  15946  3dom  16411  pwle2  16423  nninfalllem1  16434  nninfall  16435  nninfsellemqall  16441