Theorem mto 587

Description: The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses

Ref	Expression
mto.1	⊢ ¬ ψ
mto.2	⊢ (φ → ψ)

Assertion

Ref	Expression
mto	⊢ ¬ φ

Proof of Theorem mto

Step	Hyp	Ref	Expression
1		mto.2	. 2 ⊢ (φ → ψ)
2		mto.1	. . 3 ⊢ ¬ ψ
3	2	a1i 9	. 2 ⊢ (φ → ¬ ψ)
4	1, 3	pm2.65i 567	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:  mtbi  594  pm3.2ni  725  pm5.16  736  intnan  837  intnanr  838  equidqe  1422  nexr  1579  ru  2757  sspssn  3042  neldifsn  3488  nvel  3880  nlim0  4097  snnex  4147  onprc  4230  dtruex  4237  ordsoexmid  4240  nprrel  4329  0xp  4363  iprc  4543  son2lpi  4664  nfunv  4876  0fv  5151  acexmidlema  5446  acexmidlemb  5447  acexmidlemab  5449  mpt20  5516  0nnq  6348  0npr  6466  1ne0sr  6694  pnfnre  6864  mnfnre  6865  ine0  7187  inelr  7368  1nuz2  8319  0nrp  8391  bj-nvel  9352