Theorem mtoi 670

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  680  mtbiri  681  pwnss  4249  exmid1stab  4298  nsuceq0g  4515  abnex  4544  reg2exmidlema  4632  ordsuc  4661  onnmin  4666  ssnel  4667  ordtri2or2exmid  4669  ontri2orexmidim  4670  reg3exmidlemwe  4677  acexmidlemab  6011  reldmtpos  6418  dmtpos  6421  2pwuninelg  6448  onunsnss  7108  snon0  7133  nninfisol  7331  exmidomni  7340  pr2ne  7396  ltexprlemdisj  7825  recexprlemdisj  7849  caucvgprlemnkj  7885  caucvgprprlemnkltj  7908  caucvgprprlemnkeqj  7909  caucvgprprlemnjltk  7910  inelr  8763  rimul  8764  recgt0  9029  zfz1iso  11104  isprm2  12688  nprmdvds1  12711  divgcdodd  12714  coprm  12715  coseq0q4123  15557  lgsquad2lem2  15810  umgrnloop0  15967  umgrislfupgrenlem  15980  lfgrnloopen  15983  3dom  16587  pwle2  16599  nninfalllem1  16610  nninfall  16611  nninfsellemqall  16617