Theorem mtoi 670

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  681  mtbiri  682  ifeqeqxdc  3673  pwnss  4277  exmid1stab  4326  nsuceq0g  4544  abnex  4573  reg2exmidlema  4661  ordsuc  4690  onnmin  4695  ssnel  4696  ordtri2or2exmid  4698  ontri2orexmidim  4699  reg3exmidlemwe  4706  acexmidlemab  6052  reldmtpos  6497  dmtpos  6500  2pwuninelg  6527  onunsnss  7190  snon0  7215  nninfisol  7437  exmidomni  7446  pr2ne  7502  ltexprlemdisj  7937  recexprlemdisj  7961  caucvgprlemnkj  7997  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemnjltk  8022  inelr  8875  rimul  8876  recgt0  9141  zfz1iso  11238  isprm2  12839  nprmdvds1  12862  divgcdodd  12865  coprm  12866  coseq0q4123  15825  lgsquad2lem2  16081  umgrnloop0  16238  umgrislfupgrenlem  16251  lfgrnloopen  16254  3dom  16888  pwle2  16898  nninfalllem1  16912  nninfall  16913  nninfsellemqall  16919