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  2972  pssirr  4058  vn0  4298  reu0  4316  neldifsn  4762  axnulALT  5269  nvel  5284  nvelOLD  5287  nfnid  5348  nprrel  5722  0xp  5762  xp0  5763  nrelv  5788  son2lpi  6130  nlim0  6425  snsn0non  6491  onnev  6493  nfunv  6573  dffv3  6881  mpo0  7504  onprc  7783  ordeleqon  7787  onuninsuci  7842  orduninsuc  7845  iprc  7914  poxp2  8145  poxp3  8152  tfrlem13  8383  tfrlem14  8384  tfrlem16  8386  tfr2b  8389  tz7.44lem1  8398  nlim1  8480  nlim2  8481  sdomn2lp  9111  canth2  9125  map2xp  9142  ordfin  9207  snnen2o  9212  1sdom2dom  9221  fi0  9387  nelaneq  9571  sucprcregOLD  9576  rankxplim3  9860  alephnbtwn2  10072  alephprc  10099  unialeph  10101  kmlem16  10165  cfsuc  10256  nd1  10589  nd2  10590  canthp1lem2  10655  0nnq  10926  1ne0sr  11098  pnfnre  11267  mnfnre  11269  ine0  11666  recgt0ii  12138  inelr  12225  0nnn  12289  nnunb  12517  nn0nepnf  12602  indstr  12958  1nuz2  12966  0nrp  13071  lsw0  14622  egt2lt3  16286  ruc  16323  odd2np1  16423  divalglem5  16479  bitsf1  16528  0nprm  16760  structcnvcnv  17237  fvsetsid  17252  fnpr2ob  17636  oduclatb  18587  0g0  18749  psgnunilem3  19612  zringndrg  21670  00ply1bas  22451  0ntop  23114  topnex  23205  bwth  23619  ustn0  24431  vitalilem5  25824  deg1nn0clb  26300  aaliou3lem9  26566  sinhalfpilem  26681  logdmn0  26858  dvlog  26869  ppiltx  27394  dchrisum0fno1  27728  nosgnn0i  27876  ltssolem1  27892  nolt02o  27912  nogt01o  27913  noprc  28002  oldirr  28136  leftirr  28137  rightirr  28138  axlowdim1  29366  topnfbey  30893  0ngrp  30936  dmadjrnb  32331  neldifpr1  32952  neldifpr2  32953  1nei  33154  nn0xmulclb  33188  gsummulsubdishift1  33454  ply1coedeg  33945  cos9thpinconstr  34247  trisecnconstr  34248  ballotlem2  34946  bnj1304  35274  bnj110  35313  bnj98  35322  bnj1523  35526  axnulALT2  35536  fineqvinfep  35597  subfacp1lem5  35715  msrrcl  36074  linedegen  36674  rankeq1o  36702  neufal  36976  neutru  36977  unqsym1  36995  onpsstopbas  37000  ordcmp  37017  onint1  37019  elttcirr  37101  bj-ru  37639  bj-1nel0  37649  bj-0nelsngl  37666  bj-vn0ALT  37767  bj-0nmoore  37813  bj-ccinftydisj  37916  relowlpssretop  38069  poimirlem16  38346  poimirlem17  38347  poimirlem18  38348  poimirlem19  38349  poimirlem20  38350  poimirlem22  38352  poimirlem30  38360  zrdivrng  38664  prtlem400  39704  equidqe  39756  sn-inelr  43321  eldioph4b  43598  jm2.23  43783  ttac  43823  sucomisnotcard  44330  clsk1indlem1  44831  rusbcALT  45208  nimnbi  45941  nimnbi2  45942  fouriersw  47005  nthrucw  47667  cjnpoly  47686  tannpoly  47687  sinnpoly  47688  aibnbna  47703  dtrucor3  49636  fonex  49704  alseu-no-surprise  50675