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  4202  exmid1stab  4251  nsuceq0g  4464  abnex  4493  reg2exmidlema  4581  ordsuc  4610  onnmin  4615  ssnel  4616  ordtri2or2exmid  4618  ontri2orexmidim  4619  reg3exmidlemwe  4626  acexmidlemab  5937  reldmtpos  6338  dmtpos  6341  2pwuninelg  6368  onunsnss  7013  snon0  7036  nninfisol  7234  exmidomni  7243  pr2ne  7299  ltexprlemdisj  7718  recexprlemdisj  7742  caucvgprlemnkj  7778  caucvgprprlemnkltj  7801  caucvgprprlemnkeqj  7802  caucvgprprlemnjltk  7803  inelr  8656  rimul  8657  recgt0  8922  zfz1iso  10984  isprm2  12381  nprmdvds1  12404  divgcdodd  12407  coprm  12408  coseq0q4123  15248  lgsquad2lem2  15501  pwle2  15868  nninfalllem1  15878  nninfall  15879  nninfsellemqall  15885