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  1645  nexr  1822  equidqe  2114  ru  2991  neldifsn  3752  axnulALT  4148  nvel  4154  nfnid  4203  nlim0  4449  snsn0non  4510  snnex  4523  onprc  4575  ordeleqon  4579  onuninsuci  4630  orduninsuc  4633  nprrel  4730  xp0r  4767  iprc  4942  son2lpi  5070  son2lpiOLD  5075  nfunv  5251  mpt20  6161  tfrlem13  6402  tfrlem14  6403  tfrlem16  6405  tfr2b  6408  tz7.44lem1  6414  sdomn2lp  6996  canth2  7010  map2xp  7027  fi0  7169  cantnf  7391  rankxplim3  7547  alephnbtwn2  7695  alephprc  7722  unialeph  7724  kmlem16  7787  cfsuc  7879  nd1  8205  nd2  8206  canthp1lem2  8271  0nnq  8544  1ne0sr  8714  pnfnre  8870  mnfnre  8871  ine0  9211  recgt0ii  9658  inelr  9732  nnunb  9957  indstr  10283  1nuz2  10289  0nrp  10380  egt2lt3  12480  ruc  12517  odd2np1  12583  divalglem5  12592  bitsfzolem  12621  bitsfzo  12622  bitsinv1lem  12628  bitsf1  12633  smu02  12674  structcnvcnv  13155  strlemor1  13231  oduclatb  14244  0g0  14382  00ply1bas  16314  0ntop  16647  vitalilem5  18963  deg1nn0clb  19472  aaliou3lem9  19726  sinhalfpilem  19830  logdmn0  19983  dvlog  19994  ppiltx  20411  dchrisum0fno1  20656  0ngrp  20872  zrdivrng  21093  vcoprne  21129  dmadjrnb  22482  subfacp1lem5  23122  nosgnn0i  23716  axsltsolem1  23725  noprc  23738  funpartfv  23893  axlowdim1  23997  linedegen  24176  rankeq1o  24211  unnf  24256  unnt  24257  unqsym1  24274  amosym1  24275  onpsstopbas  24279  ordcmp  24296  onint1  24298  inpc  24688  zrfld  24846  prtlem400  26149  eldioph4b  26305  jm2.23  26500  ttac  26540  psgnunilem3  26830  rusbcALT  27050  compneOLD  27054  bnj521  28044  bnj1304  28131  bnj110  28169  bnj98  28178  bnj1523  28380  ax9lem1  28419
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator