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

Theorem mto 180
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. Inference associated with con3i 141. (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 177 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  184  mtbi  300  pm3.2ni  863  intnan  923  intnanr  924  nexr  1924  nonconne  2633  ru  3300  neldifsn  4126  axnulALT  4551  nvel  4562  nfnid  4649  nprrel  4895  0xp  4933  son2lpi  5246  nlim0  5499  snsn0non  5559  nfunv  5631  dffv3  5876  mpt20  6374  snnex  6610  onprc  6624  ordeleqon  6628  onuninsuci  6680  orduninsuc  6683  iprc  6741  tfrlem13  7118  tfrlem14  7119  tfrlem16  7121  tfr2b  7124  tz7.44lem1  7133  sdomn2lp  7719  canth2  7733  map2xp  7750  fi0  7942  sucprcreg  8122  rankxplim3  8359  alephnbtwn2  8509  alephprc  8536  unialeph  8538  kmlem16  8601  cfsuc  8693  nd1  9018  nd2  9019  canthp1lem2  9084  0nnq  9355  1ne0sr  9526  pnfnre  9688  mnfnre  9689  ine0  10060  recgt0ii  10518  inelr  10605  nnunb  10871  indstr  11233  1nuz2  11240  0nrp  11340  zgt1rpn0n1  11346  lsw0  12714  egt2lt3  14255  ruc  14292  n2dvds1  14351  odd2np1  14362  divalglem5OLD  14373  divalglem5  14374  bitsf1  14417  structcnvcnv  15129  fvsetsid  15145  strlemor1  15214  meet0  16380  join0  16381  oduclatb  16387  0g0  16503  psgnunilem3  17134  00ply1bas  18830  0ntop  19931  bwth  20421  ustn0  21231  vitalilem5  22566  deg1nn0clb  23035  aaliou3lem9  23302  sinhalfpilem  23414  logdmn0  23581  dvlog  23592  ppiltx  24100  dchrisum0fno1  24345  axlowdim1  24985  wlkntrllem3  25287  spthispth  25299  topnfbey  25902  0ngrp  25935  zrdivrng  26156  vcoprne  26194  dmadjrnb  27555  ballotlem2  29327  bnj521  29551  bnj1304  29637  bnj110  29675  bnj98  29684  bnj1523  29886  subfacp1lem5  29913  msrrcl  30187  nosgnn0i  30551  sltsolem1  30560  noprc  30573  linedegen  30913  rankeq1o  30941  unnf  31070  unnt  31071  unqsym1  31088  amosym1  31089  onpsstopbas  31093  ordcmp  31110  onint1  31112  bj-babygodel  31188  bj-ru0  31503  bj-ru  31505  bj-1nel0  31513  bj-0nelsngl  31531  bj-ccinftydisj  31617  relowlpssretop  31729  poimirlem16  31918  poimirlem17  31919  poimirlem18  31920  poimirlem19  31921  poimirlem20  31922  poimirlem22  31924  poimirlem30  31932  prtlem400  32408  equidqe  32460  eldioph4b  35621  jm2.23  35819  ttac  35859  rusbcALT  36696  fouriersw  37963  aibnbna  38254
  Copyright terms: Public domain W3C validator