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

Theorem mto 170
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" - remark in [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 168 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt3  174  mtbi  291  pm3.2ni  829  intnan  882  intnanr  883  equidOLD  1690  nexr  1777  equidqe  2251  ru  3161  neldifsn  3930  axnulALT  4337  nvel  4343  nfnid  4394  nlim0  4640  snsn0non  4701  snnex  4714  onprc  4766  ordeleqon  4770  onuninsuci  4821  orduninsuc  4824  nprrel  4921  xp0r  4957  iprc  5135  son2lpi  5263  son2lpiOLD  5268  nfunv  5485  dffv3  5725  mpt20  6428  tfrlem13  6652  tfrlem14  6653  tfrlem16  6655  tfr2b  6658  tz7.44lem1  6664  sdomn2lp  7247  canth2  7261  map2xp  7278  fi0  7426  cantnf  7650  rankxplim3  7806  alephnbtwn2  7954  alephprc  7981  unialeph  7983  kmlem16  8046  cfsuc  8138  nd1  8463  nd2  8464  canthp1lem2  8529  0nnq  8802  1ne0sr  8972  pnfnre  9128  mnfnre  9129  ine0  9470  recgt0ii  9917  inelr  9991  nnunb  10218  indstr  10546  1nuz2  10552  0nrp  10643  egt2lt3  12806  ruc  12843  odd2np1  12909  divalglem5  12918  bitsfzolem  12947  bitsfzo  12948  bitsinv1lem  12954  bitsf1  12959  structcnvcnv  13481  strlemor1  13557  oduclatb  14572  0g0  14710  00ply1bas  16635  0ntop  16979  ustn0  18251  vitalilem5  19505  deg1nn0clb  20014  aaliou3lem9  20268  sinhalfpilem  20375  logdmn0  20532  dvlog  20543  ppiltx  20961  dchrisum0fno1  21206  wlkntrllem3  21562  spthispth  21574  0ngrp  21800  zrdivrng  22021  vcoprne  22059  dmadjrnb  23410  rnlogblem  24400  ballotlem2  24747  subfacp1lem5  24871  nosgnn0i  25615  sltsolem1  25624  noprc  25637  axlowdim1  25899  linedegen  26078  rankeq1o  26113  unnf  26158  unnt  26159  unqsym1  26176  amosym1  26177  onpsstopbas  26181  ordcmp  26198  onint1  26200  prtlem400  26720  eldioph4b  26873  jm2.23  27068  ttac  27108  psgnunilem3  27397  rusbcALT  27617  aibnbna  27851  bnj521  29105  bnj1304  29192  bnj110  29230  bnj98  29239  bnj1523  29441  ax7w11AUX7  29664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator