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

Theorem mto 188
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 150. (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 185 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  192  mtbi  311  pm3.2ni  917  intnan  980  intnanr  981  nexr  2100  nonconne  2835  ru  3467  neldifsn  4354  axnulALT  4820  nvel  4830  nfnid  4927  nprrel  5195  0xp  5233  son2lpi  5559  nlim0  5821  snsn0non  5884  nfunv  5959  dffv3  6225  mpt20  6767  snnexOLD  7009  onprc  7026  ordeleqon  7030  onuninsuci  7082  orduninsuc  7085  iprc  7143  tfrlem13  7531  tfrlem14  7532  tfrlem16  7534  tfr2b  7537  tz7.44lem1  7546  sdomn2lp  8140  canth2  8154  map2xp  8171  fi0  8367  sucprcreg  8544  rankxplim3  8782  alephnbtwn2  8933  alephprc  8960  unialeph  8962  kmlem16  9025  cfsuc  9117  nd1  9447  nd2  9448  canthp1lem2  9513  0nnq  9784  1ne0sr  9955  pnfnre  10119  mnfnre  10120  ine0  10503  recgt0ii  10967  inelr  11048  nnunb  11326  nn0nepnf  11409  indstr  11794  1nuz2  11802  0nrp  11903  zgt1rpn0n1  11909  lsw0  13385  egt2lt3  14978  ruc  15016  odd2np1  15112  n2dvds1  15151  divalglem5  15167  bitsf1  15215  structcnvcnv  15918  fvsetsid  15937  strlemor1OLD  16016  meet0  17184  join0  17185  oduclatb  17191  0g0  17310  psgnunilem3  17962  00ply1bas  19658  zringndrg  19886  0ntop  20758  topnex  20848  bwth  21261  ustn0  22071  vitalilem5  23426  deg1nn0clb  23895  aaliou3lem9  24150  sinhalfpilem  24260  logdmn0  24431  dvlog  24442  ppiltx  24948  dchrisum0fno1  25245  axlowdim1  25884  topnfbey  27455  0ngrp  27493  dmadjrnb  28893  ballotlem2  30678  bnj521  30931  bnj1304  31016  bnj110  31054  bnj98  31063  bnj1523  31265  subfacp1lem5  31292  msrrcl  31566  nosgnn0i  31937  sltsolem1  31951  nolt02o  31970  noprc  32020  linedegen  32375  rankeq1o  32403  unnf  32531  unnt  32532  unqsym1  32549  amosym1  32550  onpsstopbas  32554  ordcmp  32571  onint1  32573  bj-babygodel  32713  bj-ru0  33057  bj-ru  33059  bj-1nel0  33066  bj-0nelsngl  33084  bj-0nmoore  33192  bj-ccinftydisj  33230  relowlpssretop  33342  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem30  33569  zrdivrng  33882  prtlem400  34474  equidqe  34526  eldioph4b  37692  jm2.23  37880  ttac  37920  clsk1indlem1  38660  rusbcALT  38957  fouriersw  40766  aibnbna  41394
  Copyright terms: Public domain W3C validator