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  32680  nn0xmulclb  32714  cos9thpinconstr  33758  trisecnconstr  33759  ballotlem2  34457  bnj1304  34786  bnj110  34825  bnj98  34834  bnj1523  35038  subfacp1lem5  35161  msrrcl  35520  linedegen  36121  rankeq1o  36149  neufal  36384  neutru  36385  unqsym1  36403  onpsstopbas  36408  ordcmp  36425  onint1  36427  bj-ru  36922  bj-1nel0  36932  bj-0nelsngl  36949  bj-0nmoore  37090  bj-ccinftydisj  37191  relowlpssretop  37342  poimirlem16  37620  poimirlem17  37621  poimirlem18  37622  poimirlem19  37623  poimirlem20  37624  poimirlem22  37626  poimirlem30  37634  zrdivrng  37937  prtlem400  38853  equidqe  38905  sn-inelr  42464  eldioph4b  42788  jm2.23  42973  ttac  43013  sucomisnotcard  43521  clsk1indlem1  44022  rusbcALT  44416  nimnbi  45145  nimnbi2  45146  fouriersw  46216  cjnpoly  46877  tannpoly  46878  sinnpoly  46879  aibnbna  46894  dtrucor3  48787  fonex  48855