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  2920  axnulALT  4044  nvel  4050  nfnid  4098  nlim0  4343  snsn0non  4402  snnex  4415  onprc  4467  ordeleqon  4471  onuninsuci  4522  orduninsuc  4525  nprrel  4638  xp0r  4675  iprc  4850  son2lpi  4978  son2lpiOLD  4983  nfunv  5143  mpt20  6051  tfrlem13  6292  tfrlem14  6293  tfrlem16  6295  tfr2b  6298  tz7.44lem1  6304  sdomn2lp  6885  canth2  6899  map2xp  6916  fi0  7057  cantnf  7279  rankxplim3  7435  alephnbtwn2  7583  alephprc  7610  unialeph  7612  kmlem16  7675  cfsuc  7767  nd1  8089  nd2  8090  canthp1lem2  8155  0nnq  8428  1ne0sr  8598  pnfnre  8754  mnfnre  8755  ine0  9095  recgt0ii  9542  inelr  9616  nnunb  9840  indstr  10166  1nuz2  10172  0nrp  10263  egt2lt3  12358  ruc  12395  odd2np1  12461  divalglem5  12470  bitsfzolem  12499  bitsfzo  12500  bitsinv1lem  12506  bitsf1  12511  smu02  12552  structcnvcnv  13033  strlemor1  13109  oduclatb  14092  0g0  14221  00ply1bas  16150  0ntop  16483  vitalilem5  18799  deg1nn0clb  19308  aaliou3lem9  19562  sinhalfpilem  19666  logdmn0  19819  dvlog  19830  ppiltx  20247  dchrisum0fno1  20492  0ngrp  20708  zrdivrng  20929  vcoprne  20965  dmadjrnb  22316  subfacp1lem5  22886  nosgnn0i  23480  axsltsolem1  23489  noprc  23502  funpartfv  23657  axlowdim1  23761  linedegen  23940  rankeq1o  23975  unnf  24020  unnt  24021  unqsym1  24038  amosym1  24039  onpsstopbas  24043  ordcmp  24060  onint1  24062  inpc  24443  zrfld  24601  prtlem400  25904  eldioph4b  26060  jm2.23  26255  ttac  26295  psgnunilem3  26585  rusbcALT  26806  compneOLD  26810  aibnbna  26860  bnj521  27454  bnj1304  27541  bnj110  27579  bnj98  27588  bnj1523  27790  ax9lem1  27829
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator