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 10. (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 12 . 2  |-  ( ph  ->  -.  ps )
41, 3pm2.65i 167 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  mt3  173  mtbi  291  pm3.2ni  830  intnan  885  intnanr  886  ax12o10lem1  1635  equidqe  1686  nexr  1804  ru  2965  neldifsn  3725  axnulALT  4121  nvel  4127  nfnid  4176  nlim0  4422  snsn0non  4483  snnex  4496  onprc  4548  ordeleqon  4552  onuninsuci  4603  orduninsuc  4606  nprrel  4719  xp0r  4756  iprc  4931  son2lpi  5059  son2lpiOLD  5064  nfunv  5224  mpt20  6133  tfrlem13  6374  tfrlem14  6375  tfrlem16  6377  tfr2b  6380  tz7.44lem1  6386  sdomn2lp  6968  canth2  6982  map2xp  6999  fi0  7141  cantnf  7363  rankxplim3  7519  alephnbtwn2  7667  alephprc  7694  unialeph  7696  kmlem16  7759  cfsuc  7851  nd1  8177  nd2  8178  canthp1lem2  8243  0nnq  8516  1ne0sr  8686  pnfnre  8842  mnfnre  8843  ine0  9183  recgt0ii  9630  inelr  9704  nnunb  9929  indstr  10255  1nuz2  10261  0nrp  10352  egt2lt3  12447  ruc  12484  odd2np1  12550  divalglem5  12559  bitsfzolem  12588  bitsfzo  12589  bitsinv1lem  12595  bitsf1  12600  smu02  12641  structcnvcnv  13122  strlemor1  13198  oduclatb  14211  0g0  14349  00ply1bas  16281  0ntop  16614  vitalilem5  18930  deg1nn0clb  19439  aaliou3lem9  19693  sinhalfpilem  19797  logdmn0  19950  dvlog  19961  ppiltx  20378  dchrisum0fno1  20623  0ngrp  20839  zrdivrng  21060  vcoprne  21096  dmadjrnb  22447  subfacp1lem5  23088  nosgnn0i  23682  axsltsolem1  23691  noprc  23704  funpartfv  23859  axlowdim1  23963  linedegen  24142  rankeq1o  24177  unnf  24222  unnt  24223  unqsym1  24240  amosym1  24241  onpsstopbas  24245  ordcmp  24262  onint1  24264  inpc  24645  zrfld  24803  prtlem400  26106  eldioph4b  26262  jm2.23  26457  ttac  26497  psgnunilem3  26787  rusbcALT  27008  compneOLD  27012  bnj521  27897  bnj1304  27984  bnj110  28022  bnj98  28031  bnj1523  28233  equidK  28235  ax12o10lem1X  28282  ax9lem1  28390
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator