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  4247  exmid1stab  4296  nsuceq0g  4513  abnex  4542  reg2exmidlema  4630  ordsuc  4659  onnmin  4664  ssnel  4665  ordtri2or2exmid  4667  ontri2orexmidim  4668  reg3exmidlemwe  4675  acexmidlemab  6007  reldmtpos  6414  dmtpos  6417  2pwuninelg  6444  onunsnss  7102  snon0  7125  nninfisol  7323  exmidomni  7332  pr2ne  7388  ltexprlemdisj  7816  recexprlemdisj  7840  caucvgprlemnkj  7876  caucvgprprlemnkltj  7899  caucvgprprlemnkeqj  7900  caucvgprprlemnjltk  7901  inelr  8754  rimul  8755  recgt0  9020  zfz1iso  11095  isprm2  12679  nprmdvds1  12702  divgcdodd  12705  coprm  12706  coseq0q4123  15548  lgsquad2lem2  15801  umgrnloop0  15958  umgrislfupgrenlem  15969  lfgrnloopen  15972  3dom  16523  pwle2  16535  nninfalllem1  16546  nninfall  16547  nninfsellemqall  16553