Theorem mto 197

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 194	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  201  mtbi  322  intnan  486  intnanr  487  pm3.2ni  880  ru0  2128  nexr  2193  nonconne  2937  ruOLD  3749  reu0  4320  neldifsn  4752  axnulALT  5254  nvel  5266  nfnid  5325  nprrel  5690  0xp  5729  son2lpi  6089  nlim0  6380  snsn0non  6447  onnev  6449  nfunv  6533  dffv3  6836  mpo0  7454  onprc  7734  ordeleqon  7738  onuninsuci  7796  orduninsuc  7799  iprc  7867  poxp2  8099  poxp3  8106  tfrlem13  8335  tfrlem14  8336  tfrlem16  8338  tfr2b  8341  tz7.44lem1  8350  nlim1  8430  nlim2  8431  sdomn2lp  9057  canth2  9071  map2xp  9088  snnen2o  9161  1sdom2dom  9170  fi0  9347  sucprcreg  9530  rankxplim3  9810  alephnbtwn2  10001  alephprc  10028  unialeph  10030  kmlem16  10095  cfsuc  10186  nd1  10516  nd2  10517  canthp1lem2  10582  0nnq  10853  1ne0sr  11025  pnfnre  11191  mnfnre  11193  ine0  11589  recgt0ii  12065  inelr  12152  0nnn  12198  nnunb  12414  nn0nepnf  12499  indstr  12851  1nuz2  12859  0nrp  12964  lsw0  14506  egt2lt3  16150  ruc  16187  odd2np1  16287  divalglem5  16343  bitsf1  16392  0nprm  16624  structcnvcnv  17099  fvsetsid  17114  fnpr2ob  17497  oduclatb  18442  0g0  18567  psgnunilem3  19402  zringndrg  21354  00ply1bas  22100  0ntop  22768  topnex  22859  bwth  23273  ustn0  24084  vitalilem5  25489  deg1nn0clb  25971  aaliou3lem9  26234  sinhalfpilem  26348  logdmn0  26525  dvlog  26536  ppiltx  27063  dchrisum0fno1  27398  nosgnn0i  27547  sltsolem1  27563  nolt02o  27583  nogt01o  27584  noprc  27667  oldirr  27777  leftirr  27778  rightirr  27779  axlowdim1  28862  topnfbey  30371  0ngrp  30413  dmadjrnb  31808  neldifpr1  32435  neldifpr2  32436  1nei  32633  nn0xmulclb  32667  cos9thpinconstr  33754  trisecnconstr  33755  ballotlem2  34453  bnj1304  34782  bnj110  34821  bnj98  34830  bnj1523  35034  subfacp1lem5  35144  msrrcl  35503  linedegen  36104  rankeq1o  36132  neufal  36367  neutru  36368  unqsym1  36386  onpsstopbas  36391  ordcmp  36408  onint1  36410  bj-ru  36905  bj-1nel0  36915  bj-0nelsngl  36932  bj-0nmoore  37073  bj-ccinftydisj  37174  relowlpssretop  37325  poimirlem16  37603  poimirlem17  37604  poimirlem18  37605  poimirlem19  37606  poimirlem20  37607  poimirlem22  37609  poimirlem30  37617  zrdivrng  37920  prtlem400  38836  equidqe  38888  sn-inelr  42448  eldioph4b  42772  jm2.23  42958  ttac  42998  sucomisnotcard  43506  clsk1indlem1  44007  rusbcALT  44401  nimnbi  45130  nimnbi2  45131  fouriersw  46202  cjnpoly  46863  tannpoly  46864  sinnpoly  46865  aibnbna  46880  dtrucor3  48760  fonex  48828