Theorem mtoi 674

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  685  mtbiri  686  ifeqeqxdc  3684  pwnss  4291  exmid1stab  4340  nsuceq0g  4558  abnex  4588  reg2exmidlema  4676  ordsuc  4705  onnmin  4710  ssnel  4711  ordtri2or2exmid  4713  ontri2orexmidim  4714  reg3exmidlemwe  4721  acexmidlemab  6069  reldmtpos  6514  dmtpos  6517  2pwuninelg  6544  onunsnss  7214  snon0  7239  nninfisol  7463  exmidomni  7472  pr2ne  7528  ltexprlemdisj  7963  recexprlemdisj  7987  caucvgprlemnkj  8023  caucvgprprlemnkltj  8046  caucvgprprlemnkeqj  8047  caucvgprprlemnjltk  8048  inelr  8902  rimul  8903  recgt0  9170  zfz1iso  11271  isprm2  12873  nprmdvds1  12896  divgcdodd  12899  coprm  12900  coseq0q4123  15858  lgsquad2lem2  16115  umgrnloop0  16272  umgrislfupgrenlem  16285  lfgrnloopen  16288  3dom  16932  pwle2  16942  nninfalllem1  16956  nninfall  16957  nninfsellemqall  16963