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 155. (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 196	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  204  mtbi  325  intnan  491  intnanr  492  pm3.2ni  893  ru0  2162  nexr  2228  nonconne  2970  pssirr  4057  vn0  4298  reu0  4316  neldifsn  4760  axnulALT  5267  nvel  5282  nvelOLD  5285  nfnid  5346  nprrel  5720  0xp  5760  xp0  5761  nrelv  5786  son2lpi  6128  nlim0  6421  snsn0non  6487  onnev  6489  nfunv  6569  dffv3  6877  mpo0  7495  onprc  7773  ordeleqon  7777  onuninsuci  7832  orduninsuc  7835  iprc  7904  poxp2  8135  poxp3  8142  tfrlem13  8373  tfrlem14  8374  tfrlem16  8376  tfr2b  8379  tz7.44lem1  8388  nlim1  8470  nlim2  8471  sdomn2lp  9100  canth2  9114  map2xp  9131  ordfin  9196  snnen2o  9201  1sdom2dom  9210  fi0  9376  nelaneq  9560  sucprcregOLD  9565  rankxplim3  9849  alephnbtwn2  10052  alephprc  10079  unialeph  10081  kmlem16  10145  cfsuc  10236  nd1  10567  nd2  10568  canthp1lem2  10633  0nnq  10904  1ne0sr  11076  pnfnre  11245  mnfnre  11247  ine0  11644  recgt0ii  12116  inelr  12203  0nnn  12267  nnunb  12495  nn0nepnf  12580  indstr  12935  1nuz2  12943  0nrp  13048  lsw0  14598  egt2lt3  16257  ruc  16294  odd2np1  16394  divalglem5  16450  bitsf1  16499  0nprm  16731  structcnvcnv  17208  fvsetsid  17223  fnpr2ob  17607  oduclatb  18558  0g0  18717  psgnunilem3  19561  zringndrg  21618  00ply1bas  22399  0ntop  23062  topnex  23153  bwth  23567  ustn0  24378  vitalilem5  25771  deg1nn0clb  26247  aaliou3lem9  26513  sinhalfpilem  26628  logdmn0  26805  dvlog  26816  ppiltx  27341  dchrisum0fno1  27675  nosgnn0i  27823  ltssolem1  27839  nolt02o  27859  nogt01o  27860  noprc  27949  oldirr  28083  leftirr  28084  rightirr  28085  axlowdim1  29309  topnfbey  30820  0ngrp  30863  dmadjrnb  32258  neldifpr1  32879  neldifpr2  32880  1nei  33082  nn0xmulclb  33116  gsummulsubdishift1  33388  ply1coedeg  33879  cos9thpinconstr  34181  trisecnconstr  34182  ballotlem2  34879  bnj1304  35207  bnj110  35246  bnj98  35255  bnj1523  35459  axnulALT2  35471  fineqvinfep  35538  subfacp1lem5  35676  msrrcl  36035  linedegen  36635  rankeq1o  36663  neufal  36937  neutru  36938  unqsym1  36956  onpsstopbas  36961  ordcmp  36978  onint1  36980  elttcirr  37062  bj-ru  37600  bj-1nel0  37610  bj-0nelsngl  37627  bj-vn0ALT  37728  bj-0nmoore  37774  bj-ccinftydisj  37877  relowlpssretop  38030  poimirlem16  38307  poimirlem17  38308  poimirlem18  38309  poimirlem19  38310  poimirlem20  38311  poimirlem22  38313  poimirlem30  38321  zrdivrng  38624  prtlem400  39664  equidqe  39716  sn-inelr  43281  eldioph4b  43558  jm2.23  43743  ttac  43783  sucomisnotcard  44290  clsk1indlem1  44791  rusbcALT  45168  nimnbi  45901  nimnbi2  45902  fouriersw  46965  nthrucw  47627  cjnpoly  47646  tannpoly  47647  sinnpoly  47648  aibnbna  47663  dtrucor3  49597  fonex  49665  alseu-no-surprise  50636