Theorem mtoi 623

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  632  mtbiri  633  pwnss  3959  nsuceq0g  4209  reg2exmidlema  4313  ordsuc  4342  onnmin  4347  ssnel  4348  ordtri2or2exmid  4350  reg3exmidlemwe  4357  acexmidlemab  5585  reldmtpos  5950  dmtpos  5953  2pwuninelg  5980  onunsnss  6554  snon0  6570  exmidomni  6703  pr2ne  6723  ltexprlemdisj  7068  recexprlemdisj  7092  caucvgprlemnkj  7128  caucvgprprlemnkltj  7151  caucvgprprlemnkeqj  7152  caucvgprprlemnjltk  7153  inelr  7961  rimul  7962  recgt0  8205  isprm2  10879  nprmdvds1  10901  divgcdodd  10902  coprm  10903