Theorem mtoi 664

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  674  mtbiri  675  pwnss  4160  exmid1stab  4209  nsuceq0g  4419  abnex  4448  reg2exmidlema  4534  ordsuc  4563  onnmin  4568  ssnel  4569  ordtri2or2exmid  4571  ontri2orexmidim  4572  reg3exmidlemwe  4579  acexmidlemab  5869  reldmtpos  6254  dmtpos  6257  2pwuninelg  6284  onunsnss  6916  snon0  6935  nninfisol  7131  exmidomni  7140  pr2ne  7191  ltexprlemdisj  7605  recexprlemdisj  7629  caucvgprlemnkj  7665  caucvgprprlemnkltj  7688  caucvgprprlemnkeqj  7689  caucvgprprlemnjltk  7690  inelr  8541  rimul  8542  recgt0  8807  zfz1iso  10821  isprm2  12117  nprmdvds1  12140  divgcdodd  12143  coprm  12144  coseq0q4123  14258  pwle2  14751  nninfalllem1  14760  nninfall  14761  nninfsellemqall  14767