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  4255  exmid1stab  4304  nsuceq0g  4521  abnex  4550  reg2exmidlema  4638  ordsuc  4667  onnmin  4672  ssnel  4673  ordtri2or2exmid  4675  ontri2orexmidim  4676  reg3exmidlemwe  4683  acexmidlemab  6022  reldmtpos  6462  dmtpos  6465  2pwuninelg  6492  onunsnss  7152  snon0  7177  nninfisol  7375  exmidomni  7384  pr2ne  7440  ltexprlemdisj  7869  recexprlemdisj  7893  caucvgprlemnkj  7929  caucvgprprlemnkltj  7952  caucvgprprlemnkeqj  7953  caucvgprprlemnjltk  7954  inelr  8806  rimul  8807  recgt0  9072  zfz1iso  11151  isprm2  12752  nprmdvds1  12775  divgcdodd  12778  coprm  12779  coseq0q4123  15628  lgsquad2lem2  15884  umgrnloop0  16041  umgrislfupgrenlem  16054  lfgrnloopen  16057  3dom  16691  pwle2  16703  nninfalllem1  16717  nninfall  16718  nninfsellemqall  16724