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 ⊢ ¬ 𝜑

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  204  mtbi  325  intnan  491  intnanr  492  pm3.2ni  893  ru0  2168  nexr  2234  nonconne  2976  pssirr  4065  vn0  4306  reu0  4324  neldifsn  4764  axnulALT  5269  nvel  5284  nvelOLD  5287  nfnid  5347  nprrel  5721  0xp  5761  xp0  5762  nrelv  5787  son2lpi  6129  nlim0  6422  snsn0non  6488  onnev  6490  nfunv  6570  dffv3  6878  mpo0  7496  onprc  7777  ordeleqon  7781  onuninsuci  7836  orduninsuc  7839  iprc  7908  poxp2  8139  poxp3  8146  tfrlem13  8377  tfrlem14  8378  tfrlem16  8380  tfr2b  8383  tz7.44lem1  8392  nlim1  8474  nlim2  8475  sdomn2lp  9104  canth2  9118  map2xp  9135  ordfin  9200  snnen2o  9205  1sdom2dom  9214  fi0  9380  nelaneq  9564  sucprcregOLD  9569  rankxplim3  9853  alephnbtwn2  10056  alephprc  10083  unialeph  10085  kmlem16  10149  cfsuc  10241  nd1  10572  nd2  10573  canthp1lem2  10638  0nnq  10909  1ne0sr  11081  pnfnre  11250  mnfnre  11252  ine0  11649  recgt0ii  12121  inelr  12208  0nnn  12272  nnunb  12500  nn0nepnf  12585  indstr  12940  1nuz2  12948  0nrp  13053  lsw0  14602  egt2lt3  16262  ruc  16299  odd2np1  16399  divalglem5  16455  bitsf1  16504  0nprm  16736  structcnvcnv  17213  fvsetsid  17228  fnpr2ob  17612  oduclatb  18563  0g0  18722  psgnunilem3  19566  zringndrg  21587  00ply1bas  22368  0ntop  23031  topnex  23122  bwth  23536  ustn0  24347  vitalilem5  25740  deg1nn0clb  26216  aaliou3lem9  26480  sinhalfpilem  26594  logdmn0  26771  dvlog  26782  ppiltx  27307  dchrisum0fno1  27641  nosgnn0i  27789  ltssolem1  27805  nolt02o  27825  nogt01o  27826  noprc  27915  oldirr  28049  leftirr  28050  rightirr  28051  axlowdim1  29250  topnfbey  30761  0ngrp  30804  dmadjrnb  32199  neldifpr1  32820  neldifpr2  32821  1nei  33023  nn0xmulclb  33057  gsummulsubdishift1  33329  ply1coedeg  33824  cos9thpinconstr  34126  trisecnconstr  34127  ballotlem2  34824  bnj1304  35152  bnj110  35191  bnj98  35200  bnj1523  35404  axnulALT2  35415  fineqvinfep  35461  subfacp1lem5  35575  msrrcl  35934  linedegen  36534  rankeq1o  36562  neufal  36806  neutru  36807  unqsym1  36825  onpsstopbas  36830  ordcmp  36847  onint1  36849  elttcirr  36931  bj-ru  37468  bj-1nel0  37478  bj-0nelsngl  37495  bj-vn0ALT  37596  bj-0nmoore  37642  bj-ccinftydisj  37745  relowlpssretop  37898  poimirlem16  38175  poimirlem17  38176  poimirlem18  38177  poimirlem19  38178  poimirlem20  38179  poimirlem22  38181  poimirlem30  38189  zrdivrng  38492  prtlem400  39534  equidqe  39586  sn-inelr  43151  eldioph4b  43430  jm2.23  43615  ttac  43655  sucomisnotcard  44162  clsk1indlem1  44663  rusbcALT  45040  nimnbi  45773  nimnbi2  45774  fouriersw  46837  nthrucw  47494  cjnpoly  47515  tannpoly  47516  sinnpoly  47517  aibnbna  47532  dtrucor3  49462  fonex  49530