Theorem mtoi 590

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  mtbii  599  mtbiri  600  pwnss  3912  nsuceq0g  4155  reg2exmidlema  4259  ordsuc  4287  onnmin  4292  ssnel  4293  onpsssuc  4295  ordtri2or2exmid  4296  reg3exmidlemwe  4303  acexmidlemab  5506  reldmtpos  5868  dmtpos  5871  2pwuninelg  5898  onunsnss  6355  snon0  6356  ltexprlemdisj  6704  recexprlemdisj  6728  caucvgprlemnkj  6764  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  inelr  7575  rimul  7576  recgt0  7816