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

Theorem mto 187
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 149. (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 184 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  191  mtbi  311  pm3.2ni  895  intnan  951  intnanr  952  nexr  2050  nonconne  2794  ru  3401  neldifsn  4262  axnulALT  4715  nvel  4725  nfnid  4823  nprrel  5084  0xp  5122  son2lpi  5443  nlim0  5700  snsn0non  5763  nfunv  5835  dffv3  6099  mpt20  6623  snnex  6862  onprc  6876  ordeleqon  6880  onuninsuci  6932  orduninsuc  6935  iprc  6993  tfrlem13  7373  tfrlem14  7374  tfrlem16  7376  tfr2b  7379  tz7.44lem1  7388  sdomn2lp  7984  canth2  7998  map2xp  8015  fi0  8209  sucprcreg  8389  rankxplim3  8627  alephnbtwn2  8778  alephprc  8805  unialeph  8807  kmlem16  8870  cfsuc  8962  nd1  9288  nd2  9289  canthp1lem2  9354  0nnq  9625  1ne0sr  9796  pnfnre  9960  mnfnre  9961  ine0  10344  recgt0ii  10808  inelr  10887  nnunb  11165  nn0nepnf  11248  indstr  11632  1nuz2  11640  0nrp  11741  zgt1rpn0n1  11747  lsw0  13205  egt2lt3  14773  ruc  14811  odd2np1  14903  n2dvds1  14942  divalglem5  14958  bitsf1  15006  structcnvcnv  15706  fvsetsid  15722  strlemor1  15796  meet0  16960  join0  16961  oduclatb  16967  0g0  17086  psgnunilem3  17739  00ply1bas  19431  zringndrg  19657  0ntop  20535  bwth  21023  ustn0  21834  vitalilem5  23187  deg1nn0clb  23654  aaliou3lem9  23909  sinhalfpilem  24019  logdmn0  24186  dvlog  24197  ppiltx  24703  dchrisum0fno1  25000  axlowdim1  25639  wlkntrllem3  26091  spthispth  26103  topnfbey  26717  0ngrp  26749  dmadjrnb  28149  ballotlem2  29877  bnj521  30059  bnj1304  30144  bnj110  30182  bnj98  30191  bnj1523  30393  subfacp1lem5  30420  msrrcl  30694  nosgnn0i  31056  sltsolem1  31067  noprc  31080  linedegen  31420  rankeq1o  31448  unnf  31576  unnt  31577  unqsym1  31594  amosym1  31595  onpsstopbas  31599  ordcmp  31616  onint1  31618  bj-babygodel  31761  bj-ru0  32124  bj-ru  32126  bj-1nel0  32134  bj-0nelsngl  32152  bj-topnex  32247  bj-ccinftydisj  32277  relowlpssretop  32388  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem30  32609  zrdivrng  32922  prtlem400  33173  equidqe  33225  eldioph4b  36393  jm2.23  36581  ttac  36621  clsk1indlem1  37363  rusbcALT  37662  fouriersw  39124  aibnbna  39722
  Copyright terms: Public domain W3C validator