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

Theorem mto 167
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 10 . 2  |-  ( ph  ->  -.  ps )
41, 3pm2.65i 165 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt3  171  mtbi  289  pm3.2ni  827  intnan  880  intnanr  881  equid  1662  nexr  1832  equidqe  2125  ru  3003  neldifsn  3764  axnulALT  4163  nvel  4169  nfnid  4220  nlim0  4466  snsn0non  4527  snnex  4540  onprc  4592  ordeleqon  4596  onuninsuci  4647  orduninsuc  4650  nprrel  4747  xp0r  4784  iprc  4959  son2lpi  5087  son2lpiOLD  5092  nfunv  5301  dffv3  5537  mpt20  6215  tfrlem13  6422  tfrlem14  6423  tfrlem16  6425  tfr2b  6428  tz7.44lem1  6434  sdomn2lp  7016  canth2  7030  map2xp  7047  fi0  7189  cantnf  7411  rankxplim3  7567  alephnbtwn2  7715  alephprc  7742  unialeph  7744  kmlem16  7807  cfsuc  7899  nd1  8225  nd2  8226  canthp1lem2  8291  0nnq  8564  1ne0sr  8734  pnfnre  8890  mnfnre  8891  ine0  9231  recgt0ii  9678  inelr  9752  nnunb  9977  indstr  10303  1nuz2  10309  0nrp  10400  egt2lt3  12500  ruc  12537  odd2np1  12603  divalglem5  12612  bitsfzolem  12641  bitsfzo  12642  bitsinv1lem  12648  bitsf1  12653  smu02  12694  structcnvcnv  13175  strlemor1  13251  oduclatb  14264  0g0  14402  00ply1bas  16334  0ntop  16667  vitalilem5  18983  deg1nn0clb  19492  aaliou3lem9  19746  sinhalfpilem  19850  logdmn0  20003  dvlog  20014  ppiltx  20431  dchrisum0fno1  20676  0ngrp  20894  zrdivrng  21115  vcoprne  21151  dmadjrnb  22502  rnlogblem  23416  subfacp1lem5  23730  nosgnn0i  24384  sltsolem1  24393  noprc  24406  axlowdim1  24659  linedegen  24838  rankeq1o  24873  unnf  24918  unnt  24919  unqsym1  24936  amosym1  24937  onpsstopbas  24941  ordcmp  24958  onint1  24960  inpc  25380  zrfld  25538  prtlem400  26841  eldioph4b  26997  jm2.23  27192  ttac  27232  psgnunilem3  27522  rusbcALT  27742  compneOLD  27746  wlkntrllem5  28349  spthispth  28359  bnj521  29081  bnj1304  29168  bnj110  29206  bnj98  29215  bnj1523  29417  ax9lem1  29762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator