Theorem mto 200

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 155. (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 196	1 ⊢ ¬ 𝜑

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mt3  204  mtbi  325  intnan  492  intnanr  493  pm3.2ni  894  ru0  2165  nexr  2231  nonconne  2973  pssirr  4060  vn0  4301  reu0  4319  neldifsn  4763  axnulALT  5270  nvel  5285  nvelOLD  5288  nfnid  5349  nprrel  5723  0xp  5763  xp0  5764  nrelv  5789  son2lpi  6131  nlim0  6425  snsn0non  6491  onnev  6493  nfunv  6573  dffv3  6881  mpo0  7501  onprc  7779  ordeleqon  7783  onuninsuci  7838  orduninsuc  7841  iprc  7910  poxp2  8141  poxp3  8148  tfrlem13  8379  tfrlem14  8380  tfrlem16  8382  tfr2b  8385  tz7.44lem1  8394  nlim1  8476  nlim2  8477  sdomn2lp  9106  canth2  9120  map2xp  9137  ordfin  9202  snnen2o  9207  1sdom2dom  9216  fi0  9382  nelaneq  9566  sucprcregOLD  9571  rankxplim3  9855  alephnbtwn2  10067  alephprc  10094  unialeph  10096  kmlem16  10160  cfsuc  10251  nd1  10582  nd2  10583  canthp1lem2  10648  0nnq  10919  1ne0sr  11091  pnfnre  11260  mnfnre  11262  ine0  11659  recgt0ii  12131  inelr  12218  0nnn  12282  nnunb  12510  nn0nepnf  12595  indstr  12950  1nuz2  12958  0nrp  13063  lsw0  14613  egt2lt3  16272  ruc  16309  odd2np1  16409  divalglem5  16465  bitsf1  16514  0nprm  16746  structcnvcnv  17223  fvsetsid  17238  fnpr2ob  17622  oduclatb  18573  0g0  18732  psgnunilem3  19576  zringndrg  21633  00ply1bas  22414  0ntop  23077  topnex  23168  bwth  23582  ustn0  24393  vitalilem5  25786  deg1nn0clb  26262  aaliou3lem9  26528  sinhalfpilem  26643  logdmn0  26820  dvlog  26831  ppiltx  27356  dchrisum0fno1  27690  nosgnn0i  27838  ltssolem1  27854  nolt02o  27874  nogt01o  27875  noprc  27964  oldirr  28098  leftirr  28099  rightirr  28100  axlowdim1  29324  topnfbey  30835  0ngrp  30878  dmadjrnb  32273  neldifpr1  32894  neldifpr2  32895  1nei  33097  nn0xmulclb  33131  gsummulsubdishift1  33401  ply1coedeg  33892  cos9thpinconstr  34194  trisecnconstr  34195  ballotlem2  34892  bnj1304  35220  bnj110  35259  bnj98  35268  bnj1523  35472  axnulALT2  35484  fineqvinfep  35550  subfacp1lem5  35688  msrrcl  36047  linedegen  36647  rankeq1o  36675  neufal  36949  neutru  36950  unqsym1  36968  onpsstopbas  36973  ordcmp  36990  onint1  36992  elttcirr  37074  bj-ru  37612  bj-1nel0  37622  bj-0nelsngl  37639  bj-vn0ALT  37740  bj-0nmoore  37786  bj-ccinftydisj  37889  relowlpssretop  38042  poimirlem16  38319  poimirlem17  38320  poimirlem18  38321  poimirlem19  38322  poimirlem20  38323  poimirlem22  38325  poimirlem30  38333  zrdivrng  38636  prtlem400  39676  equidqe  39728  sn-inelr  43293  eldioph4b  43570  jm2.23  43755  ttac  43795  sucomisnotcard  44302  clsk1indlem1  44803  rusbcALT  45180  nimnbi  45913  nimnbi2  45914  fouriersw  46977  nthrucw  47639  cjnpoly  47658  tannpoly  47659  sinnpoly  47660  aibnbna  47675  dtrucor3  49609  fonex  49677  alseu-no-surprise  50648