NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  mto GIF version

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
StepHypRef Expression
1 mto.2 . 2 (φψ)
2 mto.1 . . 3 ¬ ψ
32a1i 10 . 2 (φ → ¬ ψ)
41, 3pm2.65i 165 1 ¬ φ
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator