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

Theorem mto 200
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 157. (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 197 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  204  mtbi  325  intnan  490  intnanr  491  pm3.2ni  878  nexr  2190  nonconne  3002  ru  3722  noel  4250  reu0  4275  neldifsn  4688  axnulALT  5175  nvel  5187  nfnid  5244  nprrel  5579  0xp  5617  son2lpi  5959  nlim0  6221  snsn0non  6281  onnev  6283  nfunv  6361  dffv3  6645  mpo0  7222  onprc  7483  ordeleqon  7487  onuninsuci  7539  orduninsuc  7542  iprc  7604  tfrlem13  8013  tfrlem14  8014  tfrlem16  8016  tfr2b  8019  tz7.44lem1  8028  sdomn2lp  8644  canth2  8658  map2xp  8675  fi0  8872  sucprcreg  9053  rankxplim3  9298  alephnbtwn2  9487  alephprc  9514  unialeph  9516  kmlem16  9580  cfsuc  9672  nd1  10002  nd2  10003  canthp1lem2  10068  0nnq  10339  1ne0sr  10511  pnfnre  10675  mnfnre  10677  ine0  11068  recgt0ii  11539  inelr  11619  0nnn  11665  nnunb  11885  nn0nepnf  11967  indstr  12308  1nuz2  12316  0nrp  12416  lsw0  13912  egt2lt3  15555  ruc  15592  odd2np1  15686  divalglem5  15742  bitsf1  15789  0nprm  16016  structcnvcnv  16493  fvsetsid  16511  fnpr2ob  16827  oduclatb  17750  0g0  17870  psgnunilem3  18620  zringndrg  20187  00ply1bas  20873  0ntop  21514  topnex  21605  bwth  22019  ustn0  22830  vitalilem5  24220  deg1nn0clb  24695  aaliou3lem9  24950  sinhalfpilem  25060  logdmn0  25235  dvlog  25246  ppiltx  25766  dchrisum0fno1  26099  axlowdim1  26757  topnfbey  28258  0ngrp  28298  dmadjrnb  29693  neldifpr1  30309  neldifpr2  30310  1nei  30502  nn0xmulclb  30526  ballotlem2  31860  bnj521  32121  bnj1304  32205  bnj110  32244  bnj98  32253  bnj1523  32457  subfacp1lem5  32545  msrrcl  32904  nosgnn0i  33280  sltsolem1  33294  nolt02o  33313  noprc  33363  linedegen  33718  rankeq1o  33746  neufal  33868  neutru  33869  unqsym1  33887  amosym1  33888  onpsstopbas  33892  ordcmp  33909  onint1  33911  bj-ru0  34378  bj-ru  34380  bj-1nel0  34391  bj-0nelsngl  34408  bj-0nmoore  34528  bj-ccinftydisj  34629  bj-isrvec  34709  relowlpssretop  34782  poimirlem16  35072  poimirlem17  35073  poimirlem18  35074  poimirlem19  35075  poimirlem20  35076  poimirlem22  35078  poimirlem30  35086  zrdivrng  35390  prtlem400  36165  equidqe  36217  nsb  39385  sn-inelr  39583  eldioph4b  39745  jm2.23  39930  ttac  39970  clsk1indlem1  40741  rusbcALT  41136  fouriersw  42866  aibnbna  43492
  Copyright terms: Public domain W3C validator