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  881  ru0  2133  nexr  2200  nonconne  2945  ruOLD  3728  reu0  4302  neldifsn  4736  axnulALT  5240  nvel  5254  nfnid  5313  nprrel  5684  0xp  5724  xp0  5725  son2lpi  6086  nlim0  6378  snsn0non  6444  onnev  6446  nfunv  6526  dffv3  6831  mpo0  7446  onprc  7726  ordeleqon  7730  onuninsuci  7785  orduninsuc  7788  iprc  7856  poxp2  8087  poxp3  8094  tfrlem13  8323  tfrlem14  8324  tfrlem16  8326  tfr2b  8329  tz7.44lem1  8338  nlim1  8418  nlim2  8419  sdomn2lp  9048  canth2  9062  map2xp  9079  ordfin  9144  snnen2o  9149  1sdom2dom  9158  fi0  9327  nelaneq  9510  sucprcregOLD  9515  rankxplim3  9799  alephnbtwn2  9988  alephprc  10015  unialeph  10017  kmlem16  10082  cfsuc  10173  nd1  10504  nd2  10505  canthp1lem2  10570  0nnq  10841  1ne0sr  11013  pnfnre  11180  mnfnre  11182  ine0  11579  recgt0ii  12056  inelr  12143  0nnn  12207  nnunb  12427  nn0nepnf  12512  indstr  12860  1nuz2  12868  0nrp  12973  lsw0  14521  egt2lt3  16167  ruc  16204  odd2np1  16304  divalglem5  16360  bitsf1  16409  0nprm  16641  structcnvcnv  17117  fvsetsid  17132  fnpr2ob  17516  oduclatb  18467  0g0  18626  psgnunilem3  19465  zringndrg  21461  00ply1bas  22216  0ntop  22883  topnex  22974  bwth  23388  ustn0  24199  vitalilem5  25592  deg1nn0clb  26068  aaliou3lem9  26330  sinhalfpilem  26443  logdmn0  26620  dvlog  26631  ppiltx  27157  dchrisum0fno1  27491  nosgnn0i  27640  ltssolem1  27656  nolt02o  27676  nogt01o  27677  noprc  27765  oldirr  27899  leftirr  27900  rightirr  27901  axlowdim1  29045  topnfbey  30557  0ngrp  30600  dmadjrnb  31995  neldifpr1  32621  neldifpr2  32622  1nei  32828  nn0xmulclb  32862  gsummulsubdishift1  33147  ply1coedeg  33667  cos9thpinconstr  33954  trisecnconstr  33955  ballotlem2  34652  bnj1304  34980  bnj110  35019  bnj98  35028  bnj1523  35232  axnulALT2  35243  fineqvinfep  35288  subfacp1lem5  35385  msrrcl  35744  linedegen  36344  rankeq1o  36372  neufal  36607  neutru  36608  unqsym1  36626  onpsstopbas  36631  ordcmp  36648  onint1  36650  elttcirr  36732  bj-ru  37270  bj-1nel0  37280  bj-0nelsngl  37297  bj-0nmoore  37443  bj-ccinftydisj  37546  relowlpssretop  37697  poimirlem16  37974  poimirlem17  37975  poimirlem18  37976  poimirlem19  37977  poimirlem20  37978  poimirlem22  37980  poimirlem30  37988  zrdivrng  38291  prtlem400  39333  equidqe  39385  sn-inelr  42949  eldioph4b  43260  jm2.23  43445  ttac  43485  sucomisnotcard  43992  clsk1indlem1  44493  rusbcALT  44886  nimnbi  45614  nimnbi2  45615  fouriersw  46680  nthrucw  47335  cjnpoly  47352  tannpoly  47353  sinnpoly  47354  aibnbna  47369  dtrucor3  49289  fonex  49357