Theorem mtoi 589

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 588	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  598  mtbiri  599  pwnss  3903  nsuceq0g  4121  ordsuc  4241  onnmin  4244  ssnel  4245  onpsssuc  4247  acexmidlemab  5449  reldmtpos  5809  dmtpos  5812  2pwuninelg  5839  ltexprlemdisj  6579  recexprlemdisj  6601  inelr  7348  rimul  7349  recgt0  7577