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  7273  ltexprlemdisj  7692  recexprlemdisj  7716  caucvgprlemnkj  7752  caucvgprprlemnkltj  7775  caucvgprprlemnkeqj  7776  caucvgprprlemnjltk  7777  inelr  8630  rimul  8631  recgt0  8896  zfz1iso  10952  isprm2  12312  nprmdvds1  12335  divgcdodd  12338  coprm  12339  coseq0q4123  15178  lgsquad2lem2  15431  pwle2  15753  nninfalllem1  15763  nninfall  15764  nninfsellemqall  15770