Theorem mto 167

Description: The rule of modus tollens. The rule says, "if ψ is not true, and φ implies ψ, then ψ must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 8. (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 10	. 2 ⊢ (φ → ¬ ψ)
4	1, 3	pm2.65i 165	1 ⊢ ¬ φ

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem is referenced by:  mt3  171  mtbi  289  pm3.2ni  827  intnan  880  intnanr  881  equidOLD  1677  nexr  1760  equidqe  2173  ru  3045  neldifsn  3841  0cnsuc  4401  vinf  4555  0cnelphi  4597  proj1op  4600  proj2op  4601  xp0r  4842  xpnedisj  5513  epprc  5827  nenpw1pwlem2  6085  2p1e3c  6156  ncvsq  6256  0lt1c  6258  nchoice  6308  vncan  6337