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 5. (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-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  mt3  171  mtbi  289  pm3.2ni  827  intnan  880  intnanr  881  equidOLD  1677  nexr  1760  equidqe  2173  ru  3046  neldifsn  3842  0cnsuc  4402  vinf  4556  0cnelphi  4598  proj1op  4601  proj2op  4602  xp0r  4843  xpnedisj  5514  epprc  5828  nenpw1pwlem2  6086  2p1e3c  6157  ncvsq  6257  0lt1c  6259  nchoice  6309  vncan  6338