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  3909  nsuceq0g  4142  ordsuc  4272  onnmin  4277  ssnel  4278  onpsssuc  4280  ordtri2or2exmid  4281  acexmidlemab  5484  reldmtpos  5846  dmtpos  5849  2pwuninelg  5876  ltexprlemdisj  6676  recexprlemdisj  6700  caucvgprlemnkj  6736  caucvgprprlemnkltj  6759  caucvgprprlemnkeqj  6760  caucvgprprlemnjltk  6761  inelr  7542  rimul  7543  recgt0  7783