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  4193  exmid1stab  4242  nsuceq0g  4454  abnex  4483  reg2exmidlema  4571  ordsuc  4600  onnmin  4605  ssnel  4606  ordtri2or2exmid  4608  ontri2orexmidim  4609  reg3exmidlemwe  4616  acexmidlemab  5919  reldmtpos  6320  dmtpos  6323  2pwuninelg  6350  onunsnss  6987  snon0  7010  nninfisol  7208  exmidomni  7217  pr2ne  7271  ltexprlemdisj  7690  recexprlemdisj  7714  caucvgprlemnkj  7750  caucvgprprlemnkltj  7773  caucvgprprlemnkeqj  7774  caucvgprprlemnjltk  7775  inelr  8628  rimul  8629  recgt0  8894  zfz1iso  10950  isprm2  12310  nprmdvds1  12333  divgcdodd  12336  coprm  12337  coseq0q4123  15154  lgsquad2lem2  15407  pwle2  15729  nninfalllem1  15739  nninfall  15740  nninfsellemqall  15746