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

Theorem mto 176
Description: The rule of modus tollens. The rule says, "if 
ps is not true, and  ph implies  ps, then  ph must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mode that by denying denies" - remark in [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 5. Note that this rule is also valid in intuitionistic logic. (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 173 1  |-  -.  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mt3  180  mtbi  298  pm3.2ni  852  intnan  912  intnanr  913  nexr  1820  equidqe  2245  nonconne  2675  ru  3330  neldifsn  4154  axnulALT  4574  nvel  4586  nfnid  4676  nlim0  4936  snsn0non  4996  nprrel  5042  0xp  5080  son2lpi  5395  son2lpiOLD  5400  nfunv  5619  dffv3  5862  mpt20  6351  snnex  6590  onprc  6604  ordeleqon  6608  onuninsuci  6659  orduninsuc  6662  iprc  6719  tfrlem13  7059  tfrlem14  7060  tfrlem16  7062  tfr2b  7065  tz7.44lem1  7071  sdomn2lp  7656  canth2  7670  map2xp  7687  fi0  7880  sucprcreg  8025  cantnfOLD  8134  rankxplim3  8299  alephnbtwn2  8453  alephprc  8480  unialeph  8482  kmlem16  8545  cfsuc  8637  nd1  8962  nd2  8963  canthp1lem2  9031  0nnq  9302  1ne0sr  9473  pnfnre  9635  mnfnre  9636  ine0  9992  recgt0ii  10451  inelr  10526  nnunb  10791  indstr  11150  1nuz2  11157  0nrp  11250  egt2lt3  13800  ruc  13837  n2dvds1  13894  odd2np1  13905  divalglem5  13914  bitsf1  13955  structcnvcnv  14501  fvsetsid  14515  strlemor1  14582  meet0  15624  join0  15625  oduclatb  15631  0g0  15751  psgnunilem3  16327  00ply1bas  18080  0ntop  19209  bwth  19704  ustn0  20486  vitalilem5  21784  deg1nn0clb  22253  aaliou3lem9  22508  sinhalfpilem  22617  logdmn0  22777  dvlog  22788  ppiltx  23207  dchrisum0fno1  23452  axlowdim1  23966  wlkntrllem3  24267  spthispth  24279  0ngrp  24917  zrdivrng  25138  vcoprne  25176  dmadjrnb  26529  rnlogblem  27683  ballotlem2  28095  subfacp1lem5  28296  nosgnn0i  29024  sltsolem1  29033  noprc  29046  linedegen  29398  rankeq1o  29433  unnf  29477  unnt  29478  unqsym1  29495  amosym1  29496  onpsstopbas  29500  ordcmp  29517  onint1  29519  prtlem400  30243  eldioph4b  30377  jm2.23  30570  ttac  30610  rusbcALT  30952  aibnbna  31596  bnj521  32890  bnj1304  32975  bnj110  33013  bnj98  33022  bnj1523  33224  bj-babygodel  33291  bj-ru0  33599  bj-ru  33601  bj-1nel0  33609  bj-0nelsngl  33628  bj-ccinftydisj  33706
  Copyright terms: Public domain W3C validator