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 ⊢ ¬ 𝜑

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mt3  204  mtbi  325  intnan  492  intnanr  493  pm3.2ni  894  ru0  2164  nexr  2229  nonconne  2968  pssirr  4051  vn0  4291  reu0  4309  neldifsn  4755  axnulALT  5258  nvel  5273  nvelOLD  5276  nfnid  5337  nprrel  5710  0xp  5750  xp0  5751  nrelv  5777  son2lpi  6122  nlim0  6423  snsn0non  6489  onnev  6491  nfunv  6573  dffv3  6881  mpo0  7505  onprc  7792  ordeleqon  7796  onuninsuci  7851  orduninsuc  7854  iprc  7923  poxp2  8160  poxp3  8167  tfrlem13  8398  tfrlem14  8399  tfrlem16  8401  tfr2b  8404  tz7.44lem1  8413  nlim1  8497  nlim2  8498  sdomn2lp  9135  canth2  9149  map2xp  9166  ordfin  9231  snnen2o  9236  1sdom2dom  9245  fi0  9412  nelaneq  9596  sucprcregOLD  9601  rankxplim3  9898  alephnbtwn2  10151  alephprc  10178  unialeph  10180  kmlem16  10244  cfsuc  10335  nd1  10672  nd2  10673  canthp1lem2  10738  0nnq  11009  1ne0sr  11181  pnfnre  11350  mnfnre  11352  ine0  11751  recgt0ii  12223  inelr  12310  0nnn  12374  nnunb  12602  nn0nepnf  12687  indstr  13043  1nuz2  13051  0nrp  13157  lsw0  14710  egt2lt3  16374  ruc  16411  odd2np1  16511  divalglem5  16567  bitsf1  16616  0nprm  16853  structcnvcnv  17331  fvsetsid  17346  fnpr2ob  17730  oduclatb  18681  0g0  18844  psgnunilem3  19710  zringndrg  21774  00ply1bas  22557  0ntop  23223  topnex  23314  bwth  23728  ustn0  24540  vitalilem5  25933  deg1nn0clb  26408  rnplynfin  26630  aaliou3lem9  26677  sinhalfpilem  26792  logdmn0  26968  dvlog  26979  ppiltx  27504  dchrisum0fno1  27838  nosgnn0i  28016  ltssolem1  28032  nolt02o  28052  nogt01o  28053  noprc  28142  oldirr  28276  leftirr  28277  rightirr  28278  axlowdim1  29537  topnfbey  31070  0ngrp  31113  dmadjrnb  32508  neldifpr1  33129  neldifpr2  33130  1nei  33329  nn0xmulclb  33363  gsummulsubdishift1  33629  ply1coedeg  34121  cos9thpinconstr  34423  trisecnconstr  34424  ballotlem2  35121  bnj1304  35449  bnj110  35488  bnj98  35497  bnj1523  35701  axnulALT2  35712  fineqvinfep  35793  subfacp1lem5  35949  msrrcl  36308  linedegen  36908  rankeq1o  36932  neufal  37194  neutru  37195  unqsym1  37213  onpsstopbas  37218  ordcmp  37235  onint1  37237  elttcirr  37319  bj-ru  37857  bj-1nel0  37867  bj-0nelsngl  37884  bj-vn0ALT  37987  bj-0nmoore  38033  bj-ccinftydisj  38134  relowlpssretop  38287  poimirlem16  38554  poimirlem17  38555  poimirlem18  38556  poimirlem19  38557  poimirlem20  38558  poimirlem22  38560  poimirlem30  38568  zrdivrng  38887  prtlem400  39927  equidqe  39979  sn-inelr  43551  eldioph4b  43817  jm2.23  44002  ttac  44042  sucomisnotcard  44544  clsk1indlem1  45044  rusbcALT  45421  nimnbi  46177  nimnbi2  46178  fouriersw  47240  numtowerdt  47915  goldratval  47935  cjnpoly  47938  tannpoly  47939  sinnpoly  47940  sqrtrrnpoly  47941  sqrtnpoly  47942  aibnbna  47975  dtrucor3  49908  fonex  49976  alseu-no-surprise  50933