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

Theorem mto 181
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 142. (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 178 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  185  mtbi  304  pm3.2ni  870  intnan  930  intnanr  931  nexr  1960  nonconne  2646  ru  3277  neldifsn  4111  axnulALT  4544  nvel  4555  nfnid  4642  nprrel  4895  0xp  4933  son2lpi  5246  nlim0  5499  snsn0non  5559  nfunv  5631  dffv3  5883  mpt20  6387  snnex  6623  onprc  6637  ordeleqon  6641  onuninsuci  6693  orduninsuc  6696  iprc  6754  tfrlem13  7133  tfrlem14  7134  tfrlem16  7136  tfr2b  7139  tz7.44lem1  7148  sdomn2lp  7736  canth2  7750  map2xp  7767  fi0  7959  sucprcreg  8139  rankxplim3  8377  alephnbtwn2  8528  alephprc  8555  unialeph  8557  kmlem16  8620  cfsuc  8712  nd1  9037  nd2  9038  canthp1lem2  9103  0nnq  9374  1ne0sr  9545  pnfnre  9707  mnfnre  9708  ine0  10081  recgt0ii  10539  inelr  10626  nnunb  10893  indstr  11255  1nuz2  11262  0nrp  11362  zgt1rpn0n1  11368  lsw0  12747  egt2lt3  14306  ruc  14343  n2dvds1  14402  odd2np1  14413  divalglem5OLD  14424  divalglem5  14425  bitsf1  14468  structcnvcnv  15180  fvsetsid  15196  strlemor1  15265  meet0  16431  join0  16432  oduclatb  16438  0g0  16554  psgnunilem3  17185  00ply1bas  18881  0ntop  19983  bwth  20473  ustn0  21283  vitalilem5  22618  deg1nn0clb  23087  aaliou3lem9  23354  sinhalfpilem  23466  logdmn0  23633  dvlog  23644  ppiltx  24152  dchrisum0fno1  24397  axlowdim1  25037  wlkntrllem3  25339  spthispth  25351  topnfbey  25954  0ngrp  25987  zrdivrng  26208  vcoprne  26246  dmadjrnb  27607  ballotlem2  29369  bnj521  29593  bnj1304  29679  bnj110  29717  bnj98  29726  bnj1523  29928  subfacp1lem5  29955  msrrcl  30229  nosgnn0i  30594  sltsolem1  30605  noprc  30618  linedegen  30958  rankeq1o  30986  unnf  31115  unnt  31116  unqsym1  31133  amosym1  31134  onpsstopbas  31138  ordcmp  31155  onint1  31157  bj-babygodel  31231  bj-ru0  31581  bj-ru  31583  bj-1nel0  31591  bj-0nelsngl  31609  bj-ccinftydisj  31699  relowlpssretop  31811  poimirlem16  32000  poimirlem17  32001  poimirlem18  32002  poimirlem19  32003  poimirlem20  32004  poimirlem22  32006  poimirlem30  32014  prtlem400  32486  equidqe  32537  eldioph4b  35698  jm2.23  35895  ttac  35935  rusbcALT  36833  fouriersw  38132  aibnbna  38530  nn0nepnf  39124
  Copyright terms: Public domain W3C validator