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  2228  nonconne  2967  pssirr  4051  vn0  4291  reu0  4309  neldifsn  4755  axnulALT  5261  nvel  5276  nvelOLD  5279  nfnid  5340  nprrel  5714  0xp  5754  xp0  5755  nrelv  5780  son2lpi  6122  nlim0  6418  snsn0non  6484  onnev  6486  nfunv  6567  dffv3  6875  mpo0  7499  onprc  7778  ordeleqon  7782  onuninsuci  7837  orduninsuc  7840  iprc  7909  poxp2  8142  poxp3  8149  tfrlem13  8380  tfrlem14  8381  tfrlem16  8383  tfr2b  8386  tz7.44lem1  8395  nlim1  8477  nlim2  8478  sdomn2lp  9115  canth2  9129  map2xp  9146  ordfin  9211  snnen2o  9216  1sdom2dom  9225  fi0  9391  nelaneq  9575  sucprcregOLD  9580  rankxplim3  9864  alephnbtwn2  10076  alephprc  10103  unialeph  10105  kmlem16  10169  cfsuc  10260  nd1  10597  nd2  10598  canthp1lem2  10663  0nnq  10934  1ne0sr  11106  pnfnre  11275  mnfnre  11277  ine0  11674  recgt0ii  12146  inelr  12233  0nnn  12297  nnunb  12525  nn0nepnf  12610  indstr  12966  1nuz2  12974  0nrp  13080  lsw0  14631  egt2lt3  16295  ruc  16332  odd2np1  16432  divalglem5  16488  bitsf1  16537  0nprm  16769  structcnvcnv  17246  fvsetsid  17261  fnpr2ob  17645  oduclatb  18596  0g0  18758  psgnunilem3  19624  zringndrg  21682  00ply1bas  22465  0ntop  23131  topnex  23222  bwth  23636  ustn0  24448  vitalilem5  25841  deg1nn0clb  26316  rnplynfin  26540  aaliou3lem9  26587  sinhalfpilem  26702  logdmn0  26878  dvlog  26889  ppiltx  27414  dchrisum0fno1  27748  nosgnn0i  27896  ltssolem1  27912  nolt02o  27932  nogt01o  27933  noprc  28022  oldirr  28156  leftirr  28157  rightirr  28158  axlowdim1  29417  topnfbey  30950  0ngrp  30993  dmadjrnb  32388  neldifpr1  33009  neldifpr2  33010  1nei  33209  nn0xmulclb  33243  gsummulsubdishift1  33509  ply1coedeg  34000  cos9thpinconstr  34302  trisecnconstr  34303  ballotlem2  35001  bnj1304  35329  bnj110  35368  bnj98  35377  bnj1523  35581  axnulALT2  35591  fineqvinfep  35652  subfacp1lem5  35764  msrrcl  36123  linedegen  36724  rankeq1o  36752  neufal  37026  neutru  37027  unqsym1  37045  onpsstopbas  37050  ordcmp  37067  onint1  37069  elttcirr  37151  bj-ru  37689  bj-1nel0  37699  bj-0nelsngl  37716  bj-vn0ALT  37817  bj-0nmoore  37863  bj-ccinftydisj  37966  relowlpssretop  38119  poimirlem16  38386  poimirlem17  38387  poimirlem18  38388  poimirlem19  38389  poimirlem20  38390  poimirlem22  38392  poimirlem30  38400  zrdivrng  38704  prtlem400  39744  equidqe  39796  sn-inelr  43376  eldioph4b  43653  jm2.23  43838  ttac  43878  sucomisnotcard  44385  clsk1indlem1  44886  rusbcALT  45263  nimnbi  45996  nimnbi2  45997  fouriersw  47060  numtowerdt  47735  goldratval  47755  cjnpoly  47758  tannpoly  47759  sinnpoly  47760  sqrtrrnpoly  47761  sqrtnpoly  47762  aibnbna  47795  dtrucor3  49728  fonex  49796  alseu-no-surprise  50768