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  1646  nexr  1822  equidqe  2114  ru  2992  neldifsn  3753  axnulALT  4149  nvel  4155  nfnid  4206  nlim0  4452  snsn0non  4513  snnex  4526  onprc  4578  ordeleqon  4582  onuninsuci  4633  orduninsuc  4636  nprrel  4733  xp0r  4770  iprc  4945  son2lpi  5073  son2lpiOLD  5078  nfunv  5287  dffv3  5523  mpt20  6201  tfrlem13  6408  tfrlem14  6409  tfrlem16  6411  tfr2b  6414  tz7.44lem1  6420  sdomn2lp  7002  canth2  7016  map2xp  7033  fi0  7175  cantnf  7397  rankxplim3  7553  alephnbtwn2  7701  alephprc  7728  unialeph  7730  kmlem16  7793  cfsuc  7885  nd1  8211  nd2  8212  canthp1lem2  8277  0nnq  8550  1ne0sr  8720  pnfnre  8876  mnfnre  8877  ine0  9217  recgt0ii  9664  inelr  9738  nnunb  9963  indstr  10289  1nuz2  10295  0nrp  10386  egt2lt3  12486  ruc  12523  odd2np1  12589  divalglem5  12598  bitsfzolem  12627  bitsfzo  12628  bitsinv1lem  12634  bitsf1  12639  smu02  12680  structcnvcnv  13161  strlemor1  13237  oduclatb  14250  0g0  14388  00ply1bas  16320  0ntop  16653  vitalilem5  18969  deg1nn0clb  19478  aaliou3lem9  19732  sinhalfpilem  19836  logdmn0  19989  dvlog  20000  ppiltx  20417  dchrisum0fno1  20662  0ngrp  20880  zrdivrng  21101  vcoprne  21137  dmadjrnb  22488  rnlogblem  23403  subfacp1lem5  23717  nosgnn0i  24315  sltsolem1  24324  noprc  24337  funpartfv  24485  axlowdim1  24589  linedegen  24768  rankeq1o  24803  unnf  24848  unnt  24849  unqsym1  24866  amosym1  24867  onpsstopbas  24871  ordcmp  24888  onint1  24890  inpc  25288  zrfld  25446  prtlem400  26749  eldioph4b  26905  jm2.23  27100  ttac  27140  psgnunilem3  27430  rusbcALT  27650  compneOLD  27654  bnj521  28838  bnj1304  28925  bnj110  28963  bnj98  28972  bnj1523  29174  ax9lem1  29213
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator