MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mto Unicode version

Theorem mto 169
Description: The rule of modus tollens. The rule says, "if 
ps is not true, and  ph implies  ps, then  ps 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  |-  -.  ps
mto.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
mto  |-  -.  ph

Proof of Theorem mto
StepHypRef Expression
1 mto.2 . 2  |-  ( ph  ->  ps )
2 mto.1 . . 3  |-  -.  ps
32a1i 11 . 2  |-  ( ph  ->  -.  ps )
41, 3pm2.65i 167 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt3  173  mtbi  290  pm3.2ni  828  intnan  881  intnanr  882  equidOLD  1685  nexr  1772  equidqe  2227  ru  3124  neldifsn  3893  axnulALT  4300  nvel  4306  nfnid  4357  nlim0  4603  snsn0non  4663  snnex  4676  onprc  4728  ordeleqon  4732  onuninsuci  4783  orduninsuc  4786  nprrel  4883  xp0r  4919  iprc  5097  son2lpi  5225  son2lpiOLD  5230  nfunv  5447  dffv3  5687  mpt20  6390  tfrlem13  6614  tfrlem14  6615  tfrlem16  6617  tfr2b  6620  tz7.44lem1  6626  sdomn2lp  7209  canth2  7223  map2xp  7240  fi0  7387  cantnf  7609  rankxplim3  7765  alephnbtwn2  7913  alephprc  7940  unialeph  7942  kmlem16  8005  cfsuc  8097  nd1  8422  nd2  8423  canthp1lem2  8488  0nnq  8761  1ne0sr  8931  pnfnre  9087  mnfnre  9088  ine0  9429  recgt0ii  9876  inelr  9950  nnunb  10177  indstr  10505  1nuz2  10511  0nrp  10602  egt2lt3  12764  ruc  12801  odd2np1  12867  divalglem5  12876  bitsfzolem  12905  bitsfzo  12906  bitsinv1lem  12912  bitsf1  12917  structcnvcnv  13439  strlemor1  13515  oduclatb  14530  0g0  14668  00ply1bas  16593  0ntop  16937  ustn0  18207  vitalilem5  19461  deg1nn0clb  19970  aaliou3lem9  20224  sinhalfpilem  20331  logdmn0  20488  dvlog  20499  ppiltx  20917  dchrisum0fno1  21162  wlkntrllem3  21518  spthispth  21530  0ngrp  21756  zrdivrng  21977  vcoprne  22015  dmadjrnb  23366  rnlogblem  24356  ballotlem2  24703  subfacp1lem5  24827  nosgnn0i  25531  sltsolem1  25540  noprc  25553  axlowdim1  25806  linedegen  25985  rankeq1o  26020  unnf  26065  unnt  26066  unqsym1  26083  amosym1  26084  onpsstopbas  26088  ordcmp  26105  onint1  26107  prtlem400  26613  eldioph4b  26766  jm2.23  26961  ttac  27001  psgnunilem3  27291  rusbcALT  27511  aibnbna  27745  bnj521  28814  bnj1304  28901  bnj110  28939  bnj98  28948  bnj1523  29150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator