Theorem mto 197

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 154. (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

Step	Hyp	Ref	Expression
1		mto.2	. 2 ⊢ (𝜑 → 𝜓)
2		mto.1	. . 3 ⊢ ¬ 𝜓
3	2	a1i 11	. 2 ⊢ (𝜑 → ¬ 𝜓)
4	1, 3	pm2.65i 194	1 ⊢ ¬ 𝜑

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  201  mtbi  322  intnan  486  intnanr  487  pm3.2ni  880  ru0  2132  nexr  2197  nonconne  2942  ruOLD  3737  reu0  4311  neldifsn  4746  axnulALT  5247  nvel  5259  nfnid  5318  nprrel  5681  0xp  5721  xp0  5722  son2lpi  6083  nlim0  6375  snsn0non  6441  onnev  6443  nfunv  6523  dffv3  6828  mpo0  7441  onprc  7721  ordeleqon  7725  onuninsuci  7780  orduninsuc  7783  iprc  7851  poxp2  8083  poxp3  8090  tfrlem13  8319  tfrlem14  8320  tfrlem16  8322  tfr2b  8325  tz7.44lem1  8334  nlim1  8414  nlim2  8415  sdomn2lp  9042  canth2  9056  map2xp  9073  ordfin  9138  snnen2o  9143  1sdom2dom  9152  fi0  9321  sucprcreg  9507  rankxplim3  9791  alephnbtwn2  9980  alephprc  10007  unialeph  10009  kmlem16  10074  cfsuc  10165  nd1  10496  nd2  10497  canthp1lem2  10562  0nnq  10833  1ne0sr  11005  pnfnre  11171  mnfnre  11173  ine0  11570  recgt0ii  12046  inelr  12133  0nnn  12179  nnunb  12395  nn0nepnf  12480  indstr  12827  1nuz2  12835  0nrp  12940  lsw0  14486  egt2lt3  16129  ruc  16166  odd2np1  16266  divalglem5  16322  bitsf1  16371  0nprm  16603  structcnvcnv  17078  fvsetsid  17093  fnpr2ob  17477  oduclatb  18428  0g0  18587  psgnunilem3  19423  zringndrg  21421  00ply1bas  22178  0ntop  22847  topnex  22938  bwth  23352  ustn0  24163  vitalilem5  25567  deg1nn0clb  26049  aaliou3lem9  26312  sinhalfpilem  26426  logdmn0  26603  dvlog  26614  ppiltx  27141  dchrisum0fno1  27476  nosgnn0i  27625  sltsolem1  27641  nolt02o  27661  nogt01o  27662  noprc  27746  oldirr  27862  leftirr  27863  rightirr  27864  axlowdim1  28981  topnfbey  30493  0ngrp  30535  dmadjrnb  31930  neldifpr1  32557  neldifpr2  32558  1nei  32765  nn0xmulclb  32800  gsummulsubdishift1  33100  ply1coedeg  33619  cos9thpinconstr  33897  trisecnconstr  33898  ballotlem2  34595  bnj1304  34924  bnj110  34963  bnj98  34972  bnj1523  35176  fineqvinfep  35230  subfacp1lem5  35327  msrrcl  35686  linedegen  36286  rankeq1o  36314  neufal  36549  neutru  36550  unqsym1  36568  onpsstopbas  36573  ordcmp  36590  onint1  36592  bj-ru  37088  bj-1nel0  37098  bj-0nelsngl  37115  bj-0nmoore  37256  bj-ccinftydisj  37357  relowlpssretop  37508  poimirlem16  37776  poimirlem17  37777  poimirlem18  37778  poimirlem19  37779  poimirlem20  37780  poimirlem22  37782  poimirlem30  37790  zrdivrng  38093  prtlem400  39069  equidqe  39121  sn-inelr  42684  eldioph4b  42995  jm2.23  43180  ttac  43220  sucomisnotcard  43727  clsk1indlem1  44228  rusbcALT  44621  nimnbi  45349  nimnbi2  45350  fouriersw  46417  nthrucw  47072  cjnpoly  47077  tannpoly  47078  sinnpoly  47079  aibnbna  47094  dtrucor3  48986  fonex  49054