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  4192  exmid1stab  4241  nsuceq0g  4453  abnex  4482  reg2exmidlema  4570  ordsuc  4599  onnmin  4604  ssnel  4605  ordtri2or2exmid  4607  ontri2orexmidim  4608  reg3exmidlemwe  4615  acexmidlemab  5916  reldmtpos  6311  dmtpos  6314  2pwuninelg  6341  onunsnss  6978  snon0  7001  nninfisol  7199  exmidomni  7208  pr2ne  7259  ltexprlemdisj  7673  recexprlemdisj  7697  caucvgprlemnkj  7733  caucvgprprlemnkltj  7756  caucvgprprlemnkeqj  7757  caucvgprprlemnjltk  7758  inelr  8611  rimul  8612  recgt0  8877  zfz1iso  10933  isprm2  12285  nprmdvds1  12308  divgcdodd  12311  coprm  12312  coseq0q4123  15070  lgsquad2lem2  15323  pwle2  15643  nninfalllem1  15652  nninfall  15653  nninfsellemqall  15659