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  1684  nexr  1768  equidqe  2207  ru  3103  neldifsn  3872  axnulALT  4277  nvel  4283  nfnid  4334  nlim0  4580  snsn0non  4640  snnex  4653  onprc  4705  ordeleqon  4709  onuninsuci  4760  orduninsuc  4763  nprrel  4860  xp0r  4896  iprc  5074  son2lpi  5202  son2lpiOLD  5207  nfunv  5424  dffv3  5664  mpt20  6366  tfrlem13  6587  tfrlem14  6588  tfrlem16  6590  tfr2b  6593  tz7.44lem1  6599  sdomn2lp  7182  canth2  7196  map2xp  7213  fi0  7360  cantnf  7582  rankxplim3  7738  alephnbtwn2  7886  alephprc  7913  unialeph  7915  kmlem16  7978  cfsuc  8070  nd1  8395  nd2  8396  canthp1lem2  8461  0nnq  8734  1ne0sr  8904  pnfnre  9060  mnfnre  9061  ine0  9401  recgt0ii  9848  inelr  9922  nnunb  10149  indstr  10477  1nuz2  10483  0nrp  10574  egt2lt3  12732  ruc  12769  odd2np1  12835  divalglem5  12844  bitsfzolem  12873  bitsfzo  12874  bitsinv1lem  12880  bitsf1  12885  structcnvcnv  13407  strlemor1  13483  oduclatb  14498  0g0  14636  00ply1bas  16561  0ntop  16901  ustn0  18171  vitalilem5  19371  deg1nn0clb  19880  aaliou3lem9  20134  sinhalfpilem  20241  logdmn0  20398  dvlog  20409  ppiltx  20827  dchrisum0fno1  21072  wlkntrllem5  21417  spthispth  21427  0ngrp  21647  zrdivrng  21868  vcoprne  21906  dmadjrnb  23257  rnlogblem  24195  ballotlem2  24525  subfacp1lem5  24649  nosgnn0i  25337  sltsolem1  25346  noprc  25359  axlowdim1  25612  linedegen  25791  rankeq1o  25826  unnf  25871  unnt  25872  unqsym1  25889  amosym1  25890  onpsstopbas  25894  ordcmp  25911  onint1  25913  prtlem400  26410  eldioph4b  26563  jm2.23  26758  ttac  26798  psgnunilem3  27088  rusbcALT  27308  aibnbna  27542  bnj521  28442  bnj1304  28529  bnj110  28567  bnj98  28576  bnj1523  28778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator