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  681  mtbiri  682  pwnss  4272  exmid1stab  4321  nsuceq0g  4539  abnex  4568  reg2exmidlema  4656  ordsuc  4685  onnmin  4690  ssnel  4691  ordtri2or2exmid  4693  ontri2orexmidim  4694  reg3exmidlemwe  4701  acexmidlemab  6044  reldmtpos  6484  dmtpos  6487  2pwuninelg  6514  onunsnss  7177  snon0  7202  nninfisol  7424  exmidomni  7433  pr2ne  7489  ltexprlemdisj  7921  recexprlemdisj  7945  caucvgprlemnkj  7981  caucvgprprlemnkltj  8004  caucvgprprlemnkeqj  8005  caucvgprprlemnjltk  8006  inelr  8858  rimul  8859  recgt0  9124  zfz1iso  11213  isprm2  12814  nprmdvds1  12837  divgcdodd  12840  coprm  12841  coseq0q4123  15699  lgsquad2lem2  15955  umgrnloop0  16112  umgrislfupgrenlem  16125  lfgrnloopen  16128  3dom  16762  pwle2  16772  nninfalllem1  16786  nninfall  16787  nninfsellemqall  16793