Theorem mtoi 665

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  675  mtbiri  676  pwnss  4177  exmid1stab  4226  nsuceq0g  4436  abnex  4465  reg2exmidlema  4551  ordsuc  4580  onnmin  4585  ssnel  4586  ordtri2or2exmid  4588  ontri2orexmidim  4589  reg3exmidlemwe  4596  acexmidlemab  5890  reldmtpos  6278  dmtpos  6281  2pwuninelg  6308  onunsnss  6945  snon0  6965  nninfisol  7161  exmidomni  7170  pr2ne  7221  ltexprlemdisj  7635  recexprlemdisj  7659  caucvgprlemnkj  7695  caucvgprprlemnkltj  7718  caucvgprprlemnkeqj  7719  caucvgprprlemnjltk  7720  inelr  8571  rimul  8572  recgt0  8837  zfz1iso  10853  isprm2  12149  nprmdvds1  12172  divgcdodd  12175  coprm  12176  coseq0q4123  14712  pwle2  15207  nninfalllem1  15216  nninfall  15217  nninfsellemqall  15223