Theorem mto 199

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 195	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  203  mtbi  324  intnan  490  intnanr  491  pm3.2ni  891  ru0  2161  nexr  2227  nonconne  2969  pssirr  4056  reu0  4314  neldifsn  4752  axnulALT  5254  nvel  5269  nvelOLD  5272  nfnid  5332  nprrel  5706  0xp  5746  xp0  5747  nrelv  5772  son2lpi  6115  nlim0  6406  snsn0non  6472  onnev  6474  nfunv  6554  dffv3  6863  mpo0  7481  onprc  7761  ordeleqon  7765  onuninsuci  7820  orduninsuc  7823  iprc  7892  poxp2  8123  poxp3  8130  tfrlem13  8361  tfrlem14  8362  tfrlem16  8364  tfr2b  8367  tz7.44lem1  8376  nlim1  8458  nlim2  8459  sdomn2lp  9088  canth2  9102  map2xp  9119  ordfin  9184  snnen2o  9189  1sdom2dom  9198  fi0  9366  nelaneq  9550  sucprcregOLD  9555  rankxplim3  9839  alephnbtwn2  10028  alephprc  10055  unialeph  10057  kmlem16  10122  cfsuc  10214  nd1  10545  nd2  10546  canthp1lem2  10611  0nnq  10882  1ne0sr  11054  pnfnre  11223  mnfnre  11225  ine0  11622  recgt0ii  12098  inelr  12185  0nnn  12249  nnunb  12477  nn0nepnf  12562  indstr  12917  1nuz2  12925  0nrp  13030  lsw0  14578  egt2lt3  16238  ruc  16275  odd2np1  16375  divalglem5  16431  bitsf1  16480  0nprm  16712  structcnvcnv  17189  fvsetsid  17204  fnpr2ob  17588  oduclatb  18539  0g0  18698  psgnunilem3  19536  zringndrg  21520  00ply1bas  22301  0ntop  22965  topnex  23056  bwth  23470  ustn0  24281  vitalilem5  25674  deg1nn0clb  26150  aaliou3lem9  26414  sinhalfpilem  26528  logdmn0  26705  dvlog  26716  ppiltx  27241  dchrisum0fno1  27575  nosgnn0i  27723  ltssolem1  27739  nolt02o  27759  nogt01o  27760  noprc  27849  oldirr  27983  leftirr  27984  rightirr  27985  axlowdim1  29160  topnfbey  30671  0ngrp  30714  dmadjrnb  32109  neldifpr1  32732  neldifpr2  32733  1nei  32939  nn0xmulclb  32973  gsummulsubdishift1  33248  ply1coedeg  33785  cos9thpinconstr  34088  trisecnconstr  34089  ballotlem2  34786  bnj1304  35114  bnj110  35153  bnj98  35162  bnj1523  35366  axnulALT2  35377  fineqvinfep  35421  subfacp1lem5  35534  msrrcl  35893  linedegen  36493  rankeq1o  36521  neufal  36766  neutru  36767  unqsym1  36785  onpsstopbas  36790  ordcmp  36807  onint1  36809  elttcirr  36891  bj-ru  37429  bj-1nel0  37439  bj-0nelsngl  37456  bj-0nmoore  37602  bj-ccinftydisj  37705  relowlpssretop  37858  poimirlem16  38135  poimirlem17  38136  poimirlem18  38137  poimirlem19  38138  poimirlem20  38139  poimirlem22  38141  poimirlem30  38149  zrdivrng  38452  prtlem400  39494  equidqe  39546  sn-inelr  43109  eldioph4b  43388  jm2.23  43573  ttac  43613  sucomisnotcard  44120  clsk1indlem1  44621  rusbcALT  45014  nimnbi  45741  nimnbi2  45742  fouriersw  46805  nthrucw  47462  cjnpoly  47483  tannpoly  47484  sinnpoly  47485  aibnbna  47500  dtrucor3  49420  fonex  49488