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  2128  nexr  2193  nonconne  2937  ruOLD  3741  reu0  4312  neldifsn  4743  axnulALT  5243  nvel  5255  nfnid  5314  nprrel  5678  0xp  5718  son2lpi  6077  nlim0  6367  snsn0non  6433  onnev  6435  nfunv  6515  dffv3  6818  mpo0  7434  onprc  7714  ordeleqon  7718  onuninsuci  7773  orduninsuc  7776  iprc  7844  poxp2  8076  poxp3  8083  tfrlem13  8312  tfrlem14  8313  tfrlem16  8315  tfr2b  8318  tz7.44lem1  8327  nlim1  8407  nlim2  8408  sdomn2lp  9033  canth2  9047  map2xp  9064  snnen2o  9134  1sdom2dom  9143  fi0  9310  sucprcreg  9496  rankxplim3  9777  alephnbtwn2  9966  alephprc  9993  unialeph  9995  kmlem16  10060  cfsuc  10151  nd1  10481  nd2  10482  canthp1lem2  10547  0nnq  10818  1ne0sr  10990  pnfnre  11156  mnfnre  11158  ine0  11555  recgt0ii  12031  inelr  12118  0nnn  12164  nnunb  12380  nn0nepnf  12465  indstr  12817  1nuz2  12825  0nrp  12930  lsw0  14472  egt2lt3  16115  ruc  16152  odd2np1  16252  divalglem5  16308  bitsf1  16357  0nprm  16589  structcnvcnv  17064  fvsetsid  17079  fnpr2ob  17462  oduclatb  18413  0g0  18538  psgnunilem3  19375  zringndrg  21375  00ply1bas  22122  0ntop  22790  topnex  22881  bwth  23295  ustn0  24106  vitalilem5  25511  deg1nn0clb  25993  aaliou3lem9  26256  sinhalfpilem  26370  logdmn0  26547  dvlog  26558  ppiltx  27085  dchrisum0fno1  27420  nosgnn0i  27569  sltsolem1  27585  nolt02o  27605  nogt01o  27606  noprc  27690  oldirr  27804  leftirr  27805  rightirr  27806  axlowdim1  28904  topnfbey  30413  0ngrp  30455  dmadjrnb  31850  neldifpr1  32477  neldifpr2  32478  1nei  32681  nn0xmulclb  32715  cos9thpinconstr  33764  trisecnconstr  33765  ballotlem2  34463  bnj1304  34792  bnj110  34831  bnj98  34840  bnj1523  35044  subfacp1lem5  35167  msrrcl  35526  linedegen  36127  rankeq1o  36155  neufal  36390  neutru  36391  unqsym1  36409  onpsstopbas  36414  ordcmp  36431  onint1  36433  bj-ru  36928  bj-1nel0  36938  bj-0nelsngl  36955  bj-0nmoore  37096  bj-ccinftydisj  37197  relowlpssretop  37348  poimirlem16  37626  poimirlem17  37627  poimirlem18  37628  poimirlem19  37629  poimirlem20  37630  poimirlem22  37632  poimirlem30  37640  zrdivrng  37943  prtlem400  38859  equidqe  38911  sn-inelr  42470  eldioph4b  42794  jm2.23  42979  ttac  43019  sucomisnotcard  43527  clsk1indlem1  44028  rusbcALT  44422  nimnbi  45151  nimnbi2  45152  fouriersw  46222  cjnpoly  46883  tannpoly  46884  sinnpoly  46885  aibnbna  46900  dtrucor3  48793  fonex  48861