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

Theorem mto 186
Description: The rule of modus tollens. The rule says, "if 𝜓 is not true, and 𝜑 implies 𝜓, then 𝜑 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 148. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
mto.1 ¬ 𝜓
mto.2 (𝜑𝜓)
Assertion
Ref Expression
mto ¬ 𝜑

Proof of Theorem mto
StepHypRef Expression
1 mto.2 . 2 (𝜑𝜓)
2 mto.1 . . 3 ¬ 𝜓
32a1i 11 . 2 (𝜑 → ¬ 𝜓)
41, 3pm2.65i 183 1 ¬ 𝜑
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  190  mtbi  310  pm3.2ni  894  intnan  950  intnanr  951  nexr  2049  nonconne  2793  ru  3400  neldifsn  4261  axnulALT  4709  nvel  4720  nfnid  4818  nprrel  5074  0xp  5112  son2lpi  5430  nlim0  5686  snsn0non  5749  nfunv  5821  dffv3  6084  mpt20  6601  snnex  6840  onprc  6854  ordeleqon  6858  onuninsuci  6910  orduninsuc  6913  iprc  6971  tfrlem13  7351  tfrlem14  7352  tfrlem16  7354  tfr2b  7357  tz7.44lem1  7366  sdomn2lp  7962  canth2  7976  map2xp  7993  fi0  8187  sucprcreg  8367  rankxplim3  8605  alephnbtwn2  8756  alephprc  8783  unialeph  8785  kmlem16  8848  cfsuc  8940  nd1  9266  nd2  9267  canthp1lem2  9332  0nnq  9603  1ne0sr  9774  pnfnre  9938  mnfnre  9939  ine0  10317  recgt0ii  10781  inelr  10860  nnunb  11138  indstr  11591  1nuz2  11599  0nrp  11700  zgt1rpn0n1  11706  lsw0  13154  egt2lt3  14722  ruc  14760  odd2np1  14852  n2dvds1  14891  divalglem5  14907  bitsf1  14955  structcnvcnv  15655  fvsetsid  15671  strlemor1  15745  meet0  16909  join0  16910  oduclatb  16916  0g0  17035  psgnunilem3  17688  00ply1bas  19380  0ntop  20483  bwth  20971  ustn0  21782  vitalilem5  23132  deg1nn0clb  23599  aaliou3lem9  23854  sinhalfpilem  23964  logdmn0  24131  dvlog  24142  ppiltx  24648  dchrisum0fno1  24945  axlowdim1  25585  wlkntrllem3  25885  spthispth  25897  topnfbey  26511  0ngrp  26543  vcoprneOLD  26628  dmadjrnb  27983  ballotlem2  29711  bnj521  29893  bnj1304  29978  bnj110  30016  bnj98  30025  bnj1523  30227  subfacp1lem5  30254  msrrcl  30528  nosgnn0i  30890  sltsolem1  30901  noprc  30914  linedegen  31254  rankeq1o  31282  unnf  31410  unnt  31411  unqsym1  31428  amosym1  31429  onpsstopbas  31433  ordcmp  31450  onint1  31452  bj-babygodel  31595  bj-ru0  31948  bj-ru  31950  bj-1nel0  31958  bj-0nelsngl  31976  bj-topnex  32071  bj-ccinftydisj  32101  relowlpssretop  32212  poimirlem16  32419  poimirlem17  32420  poimirlem18  32421  poimirlem19  32422  poimirlem20  32423  poimirlem22  32425  poimirlem30  32433  zrdivrng  32746  prtlem400  32997  equidqe  33049  eldioph4b  36217  jm2.23  36405  ttac  36445  clsk1indlem1  37187  rusbcALT  37486  fouriersw  38948  aibnbna  39546  nn0nepnf  40228
  Copyright terms: Public domain W3C validator