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  18448  0g0  18573  psgnunilem3  19410  zringndrg  21410  00ply1bas  22157  0ntop  22825  topnex  22916  bwth  23330  ustn0  24141  vitalilem5  25546  deg1nn0clb  26028  aaliou3lem9  26291  sinhalfpilem  26405  logdmn0  26582  dvlog  26593  ppiltx  27120  dchrisum0fno1  27455  nosgnn0i  27604  sltsolem1  27620  nolt02o  27640  nogt01o  27641  noprc  27725  oldirr  27839  leftirr  27840  rightirr  27841  axlowdim1  28939  topnfbey  30448  0ngrp  30490  dmadjrnb  31885  neldifpr1  32512  neldifpr2  32513  1nei  32710  nn0xmulclb  32744  cos9thpinconstr  33774  trisecnconstr  33775  ballotlem2  34473  bnj1304  34802  bnj110  34841  bnj98  34850  bnj1523  35054  subfacp1lem5  35164  msrrcl  35523  linedegen  36124  rankeq1o  36152  neufal  36387  neutru  36388  unqsym1  36406  onpsstopbas  36411  ordcmp  36428  onint1  36430  bj-ru  36925  bj-1nel0  36935  bj-0nelsngl  36952  bj-0nmoore  37093  bj-ccinftydisj  37194  relowlpssretop  37345  poimirlem16  37623  poimirlem17  37624  poimirlem18  37625  poimirlem19  37626  poimirlem20  37627  poimirlem22  37629  poimirlem30  37637  zrdivrng  37940  prtlem400  38856  equidqe  38908  sn-inelr  42468  eldioph4b  42792  jm2.23  42978  ttac  43018  sucomisnotcard  43526  clsk1indlem1  44027  rusbcALT  44421  nimnbi  45150  nimnbi2  45151  fouriersw  46222  cjnpoly  46883  tannpoly  46884  sinnpoly  46885  aibnbna  46900  dtrucor3  48780  fonex  48848