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  2166  nexr  2232  nonconne  2971  pssirr  4033  noel  4286  vn0  4294  reu0  4312  neldifsn  4757  axnulALT  5264  nvel  5279  nvelOLD  5283  nfnid  5344  nprrel  5717  0xp  5758  xp0  5759  nrelv  5786  son2lpi  6140  nlim0  6449  snsn0non  6515  onnev  6517  nfunv  6601  dffv3  6912  mpo0  7536  onprc  7824  onprcr  7825  ordeleqon  7830  onuninsuci  7885  orduninsuc  7888  iprc  7957  poxp2  8197  poxp3  8204  tfrlem13  8436  tfrlem14  8437  tfrlem16  8439  tfr2b  8442  tz7.44lem1  8451  nlim1  8535  nlim2  8536  sdomn2lp  9173  canth2  9187  map2xp  9204  ordfin  9269  snnen2o  9274  1sdom2dom  9283  fi0  9449  nelaneq  9633  sucprcregOLD  9638  rankxplim3  9935  cardprcr  10099  alephnbtwn2  10190  alephprc  10217  unialeph  10219  kmlem16  10283  cfsuc  10374  nd1  10711  nd2  10712  canthp1lem2  10777  0nnq  11048  1ne0sr  11220  pnfnre  11389  mnfnre  11391  ine0  11790  recgt0ii  12263  inelr  12350  0nnn  12414  nnunb  12642  nn0nepnf  12727  indstr  13083  1nuz2  13091  0nrp  13197  lsw0  14751  egt2lt3  16418  ruc  16455  odd2np1  16555  divalglem5  16611  bitsf1  16660  0nprm  16897  structcnvcnv  17375  fvsetsid  17390  fnpr2ob  17780  oduclatb  18731  0g0  18894  psgnunilem3  19761  zringndrg  21829  00ply1bas  22612  0ntop  23278  topnex  23369  bwth  23783  ustn0  24595  vitalilem5  25988  deg1nn0clb  26463  rnplynfin  26685  aaliou3lem9  26734  sinhalfpilem  26849  logdmn0  27025  dvlog  27036  ppiltx  27561  dchrisum0fno1  27895  nosgnn0i  28073  ltssolem1  28089  nolt02o  28109  nogt01o  28110  noprc  28199  oldirr  28333  leftirr  28334  rightirr  28335  axlowdim1  29594  topnfbey  31127  0ngrp  31170  dmadjrnb  32565  neldifpr1  33227  neldifpr2  33228  1nei  33425  nn0xmulclb  33459  gsummulsubdishift1  33728  ply1coedeg  34224  cos9thpinconstr  34534  trisecnconstr  34535  ballotlem2  35232  bnj1304  35560  bnj110  35599  bnj98  35608  bnj1523  35812  axnulALT2  35825  fineqvinfep  35934  j0iso  36045  onf1oracwevd  36093  subfacp1lem5  36157  msrrcl  36516  mirimanofffr  36670  linedegen  37123  rankeq1o  37147  neufal  37409  neutru  37410  unqsym1  37428  onpsstopbas  37433  ordcmp  37450  onint1  37452  elttcirr  37534  bj-ru  38072  bj-1nel0  38082  bj-0nelsngl  38099  bj-vn0ALT  38257  bj-0nmoore  38303  bj-ccinftydisj  38402  relowlpssretop  38555  poimirlem16  38822  poimirlem17  38823  poimirlem18  38824  poimirlem19  38825  poimirlem20  38826  poimirlem22  38828  poimirlem30  38836  zrdivrng  39153  prtlem400  40193  equidqe  40245  sn-inelr  43817  eldioph4b  44084  jm2.23  44269  ttac  44309  sucomisnotcard  44806  clsk1indlem1  45306  rusbcALT  45682  nimnbi  46451  nimnbi2  46452  fouriersw  47514  numtowerdt  48189  goldratval  48209  cjnpoly  48212  tannpoly  48213  sinnpoly  48214  sqrtrrnpoly  48215  sqrtnpoly  48216  aibnbna  48249  dtrucor3  50240  fonex  50309  alseu-no-surprise  51362