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  3752  reu0  4324  neldifsn  4756  axnulALT  5259  nvel  5271  nfnid  5330  nprrel  5697  0xp  5737  son2lpi  6101  nlim0  6392  snsn0non  6459  onnev  6461  nfunv  6549  dffv3  6854  mpo0  7474  onprc  7754  ordeleqon  7758  onuninsuci  7816  orduninsuc  7819  iprc  7887  poxp2  8122  poxp3  8129  tfrlem13  8358  tfrlem14  8359  tfrlem16  8361  tfr2b  8364  tz7.44lem1  8373  nlim1  8453  nlim2  8454  sdomn2lp  9080  canth2  9094  map2xp  9111  snnen2o  9184  1sdom2dom  9194  fi0  9371  sucprcreg  9554  rankxplim3  9834  alephnbtwn2  10025  alephprc  10052  unialeph  10054  kmlem16  10119  cfsuc  10210  nd1  10540  nd2  10541  canthp1lem2  10606  0nnq  10877  1ne0sr  11049  pnfnre  11215  mnfnre  11217  ine0  11613  recgt0ii  12089  inelr  12176  0nnn  12222  nnunb  12438  nn0nepnf  12523  indstr  12875  1nuz2  12883  0nrp  12988  lsw0  14530  egt2lt3  16174  ruc  16211  odd2np1  16311  divalglem5  16367  bitsf1  16416  0nprm  16648  structcnvcnv  17123  fvsetsid  17138  fnpr2ob  17521  oduclatb  18466  0g0  18591  psgnunilem3  19426  zringndrg  21378  00ply1bas  22124  0ntop  22792  topnex  22883  bwth  23297  ustn0  24108  vitalilem5  25513  deg1nn0clb  25995  aaliou3lem9  26258  sinhalfpilem  26372  logdmn0  26549  dvlog  26560  ppiltx  27087  dchrisum0fno1  27422  nosgnn0i  27571  sltsolem1  27587  nolt02o  27607  nogt01o  27608  noprc  27691  oldirr  27801  leftirr  27802  rightirr  27803  axlowdim1  28886  topnfbey  30398  0ngrp  30440  dmadjrnb  31835  neldifpr1  32462  neldifpr2  32463  1nei  32660  nn0xmulclb  32694  cos9thpinconstr  33781  trisecnconstr  33782  ballotlem2  34480  bnj1304  34809  bnj110  34848  bnj98  34857  bnj1523  35061  subfacp1lem5  35171  msrrcl  35530  linedegen  36131  rankeq1o  36159  neufal  36394  neutru  36395  unqsym1  36413  onpsstopbas  36418  ordcmp  36435  onint1  36437  bj-ru  36932  bj-1nel0  36942  bj-0nelsngl  36959  bj-0nmoore  37100  bj-ccinftydisj  37201  relowlpssretop  37352  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem30  37644  zrdivrng  37947  prtlem400  38863  equidqe  38915  sn-inelr  42475  eldioph4b  42799  jm2.23  42985  ttac  43025  sucomisnotcard  43533  clsk1indlem1  44034  rusbcALT  44428  nimnbi  45157  nimnbi2  45158  fouriersw  46229  cjnpoly  46890  tannpoly  46891  sinnpoly  46892  aibnbna  46907  dtrucor3  48787  fonex  48855