NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  mto Unicode 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 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
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-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  6255  0lt1c  6257  nchoice  6306
  Copyright terms: Public domain W3C validator