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  2165  nexr  2231  nonconne  2970  pssirr  4032  noel  4285  vn0  4293  reu0  4311  neldifsn  4754  axnulALT  5260  nvel  5275  nvelOLD  5279  nfnid  5340  nprrel  5713  0xp  5754  xp0  5755  nrelv  5781  son2lpi  6127  nlim0  6429  snsn0non  6495  onnev  6497  nfunv  6581  dffv3  6889  mpo0  7512  onprc  7799  ordeleqon  7803  onuninsuci  7858  orduninsuc  7861  iprc  7930  poxp2  8170  poxp3  8177  tfrlem13  8409  tfrlem14  8410  tfrlem16  8412  tfr2b  8415  tz7.44lem1  8424  nlim1  8508  nlim2  8509  sdomn2lp  9146  canth2  9160  map2xp  9177  ordfin  9242  snnen2o  9247  1sdom2dom  9256  fi0  9422  nelaneq  9606  sucprcregOLD  9611  rankxplim3  9908  alephnbtwn2  10161  alephprc  10188  unialeph  10190  kmlem16  10254  cfsuc  10345  nd1  10682  nd2  10683  canthp1lem2  10748  0nnq  11019  1ne0sr  11191  pnfnre  11360  mnfnre  11362  ine0  11761  recgt0ii  12233  inelr  12320  0nnn  12384  nnunb  12612  nn0nepnf  12697  indstr  13053  1nuz2  13061  0nrp  13167  lsw0  14720  egt2lt3  16386  ruc  16423  odd2np1  16523  divalglem5  16579  bitsf1  16628  0nprm  16865  structcnvcnv  17343  fvsetsid  17358  fnpr2ob  17742  oduclatb  18693  0g0  18856  psgnunilem3  19722  zringndrg  21786  00ply1bas  22569  0ntop  23235  topnex  23326  bwth  23740  ustn0  24552  vitalilem5  25945  deg1nn0clb  26420  rnplynfin  26642  aaliou3lem9  26689  sinhalfpilem  26804  logdmn0  26980  dvlog  26991  ppiltx  27516  dchrisum0fno1  27850  nosgnn0i  28028  ltssolem1  28044  nolt02o  28064  nogt01o  28065  noprc  28154  oldirr  28288  leftirr  28289  rightirr  28290  axlowdim1  29549  topnfbey  31082  0ngrp  31125  dmadjrnb  32520  neldifpr1  33183  neldifpr2  33184  1nei  33382  nn0xmulclb  33416  gsummulsubdishift1  33682  ply1coedeg  34174  cos9thpinconstr  34476  trisecnconstr  34477  ballotlem2  35174  bnj1304  35502  bnj110  35541  bnj98  35550  bnj1523  35754  axnulALT2  35767  fineqvinfep  35864  j0iso  35958  onf1oracwevd  36006  subfacp1lem5  36070  msrrcl  36429  onprcr  36583  cardprcr  36585  linedegen  37035  rankeq1o  37059  neufal  37321  neutru  37322  unqsym1  37340  onpsstopbas  37345  ordcmp  37362  onint1  37364  elttcirr  37446  bj-ru  37984  bj-1nel0  37994  bj-0nelsngl  38011  bj-vn0ALT  38126  bj-0nmoore  38172  bj-ccinftydisj  38274  relowlpssretop  38427  poimirlem16  38694  poimirlem17  38695  poimirlem18  38696  poimirlem19  38697  poimirlem20  38698  poimirlem22  38700  poimirlem30  38708  zrdivrng  39027  prtlem400  40067  equidqe  40119  sn-inelr  43691  eldioph4b  43958  jm2.23  44143  ttac  44183  sucomisnotcard  44685  clsk1indlem1  45185  rusbcALT  45561  nimnbi  46317  nimnbi2  46318  fouriersw  47380  numtowerdt  48055  goldratval  48075  cjnpoly  48078  tannpoly  48079  sinnpoly  48080  sqrtrrnpoly  48081  sqrtnpoly  48082  aibnbna  48115  dtrucor3  50048  fonex  50117  alseu-no-surprise  51148