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  6012  reldmtpos  6419  dmtpos  6422  2pwuninelg  6449  onunsnss  7109  snon0  7134  nninfisol  7332  exmidomni  7341  pr2ne  7397  ltexprlemdisj  7826  recexprlemdisj  7850  caucvgprlemnkj  7886  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnjltk  7911  inelr  8764  rimul  8765  recgt0  9030  zfz1iso  11106  isprm2  12694  nprmdvds1  12717  divgcdodd  12720  coprm  12721  coseq0q4123  15564  lgsquad2lem2  15817  umgrnloop0  15974  umgrislfupgrenlem  15987  lfgrnloopen  15990  3dom  16613  pwle2  16625  nninfalllem1  16636  nninfall  16637  nninfsellemqall  16643