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  2199  nonconne  2944  ruOLD  3739  reu0  4313  neldifsn  4748  axnulALT  5249  nvel  5261  nfnid  5320  nprrel  5683  0xp  5723  xp0  5724  son2lpi  6085  nlim0  6377  snsn0non  6443  onnev  6445  nfunv  6525  dffv3  6830  mpo0  7443  onprc  7723  ordeleqon  7727  onuninsuci  7782  orduninsuc  7785  iprc  7853  poxp2  8085  poxp3  8092  tfrlem13  8321  tfrlem14  8322  tfrlem16  8324  tfr2b  8327  tz7.44lem1  8336  nlim1  8416  nlim2  8417  sdomn2lp  9044  canth2  9058  map2xp  9075  ordfin  9140  snnen2o  9145  1sdom2dom  9154  fi0  9323  sucprcreg  9509  rankxplim3  9793  alephnbtwn2  9982  alephprc  10009  unialeph  10011  kmlem16  10076  cfsuc  10167  nd1  10498  nd2  10499  canthp1lem2  10564  0nnq  10835  1ne0sr  11007  pnfnre  11173  mnfnre  11175  ine0  11572  recgt0ii  12048  inelr  12135  0nnn  12181  nnunb  12397  nn0nepnf  12482  indstr  12829  1nuz2  12837  0nrp  12942  lsw0  14488  egt2lt3  16131  ruc  16168  odd2np1  16268  divalglem5  16324  bitsf1  16373  0nprm  16605  structcnvcnv  17080  fvsetsid  17095  fnpr2ob  17479  oduclatb  18430  0g0  18589  psgnunilem3  19425  zringndrg  21423  00ply1bas  22180  0ntop  22849  topnex  22940  bwth  23354  ustn0  24165  vitalilem5  25569  deg1nn0clb  26051  aaliou3lem9  26314  sinhalfpilem  26428  logdmn0  26605  dvlog  26616  ppiltx  27143  dchrisum0fno1  27478  nosgnn0i  27627  ltssolem1  27643  nolt02o  27663  nogt01o  27664  noprc  27752  oldirr  27886  leftirr  27887  rightirr  27888  axlowdim1  29032  topnfbey  30544  0ngrp  30586  dmadjrnb  31981  neldifpr1  32608  neldifpr2  32609  1nei  32816  nn0xmulclb  32851  gsummulsubdishift1  33151  ply1coedeg  33670  cos9thpinconstr  33948  trisecnconstr  33949  ballotlem2  34646  bnj1304  34975  bnj110  35014  bnj98  35023  bnj1523  35227  fineqvinfep  35281  subfacp1lem5  35378  msrrcl  35737  linedegen  36337  rankeq1o  36365  neufal  36600  neutru  36601  unqsym1  36619  onpsstopbas  36624  ordcmp  36641  onint1  36643  bj-ru  37145  bj-1nel0  37155  bj-0nelsngl  37172  bj-0nmoore  37317  bj-ccinftydisj  37418  relowlpssretop  37569  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  poimirlem30  37851  zrdivrng  38154  prtlem400  39140  equidqe  39192  sn-inelr  42752  eldioph4b  43063  jm2.23  43248  ttac  43288  sucomisnotcard  43795  clsk1indlem1  44296  rusbcALT  44689  nimnbi  45417  nimnbi2  45418  fouriersw  46485  nthrucw  47140  cjnpoly  47145  tannpoly  47146  sinnpoly  47147  aibnbna  47162  dtrucor3  49054  fonex  49122