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  2127  nexr  2192  nonconne  2944  ruOLD  3764  reu0  4336  neldifsn  4768  axnulALT  5274  nvel  5286  nfnid  5345  nprrel  5713  0xp  5753  son2lpi  6117  nlim0  6412  snsn0non  6478  onnev  6480  nfunv  6568  dffv3  6871  mpo0  7490  onprc  7770  ordeleqon  7774  onuninsuci  7833  orduninsuc  7836  iprc  7905  poxp2  8140  poxp3  8147  tfrlem13  8402  tfrlem14  8403  tfrlem16  8405  tfr2b  8408  tz7.44lem1  8417  nlim1  8499  nlim2  8500  sdomn2lp  9128  canth2  9142  map2xp  9159  snnen2o  9243  1sdom2dom  9253  fi0  9430  sucprcreg  9613  rankxplim3  9893  alephnbtwn2  10084  alephprc  10111  unialeph  10113  kmlem16  10178  cfsuc  10269  nd1  10599  nd2  10600  canthp1lem2  10665  0nnq  10936  1ne0sr  11108  pnfnre  11274  mnfnre  11276  ine0  11670  recgt0ii  12146  inelr  12228  0nnn  12274  nnunb  12495  nn0nepnf  12580  indstr  12930  1nuz2  12938  0nrp  13042  lsw0  14581  egt2lt3  16222  ruc  16259  odd2np1  16358  divalglem5  16414  bitsf1  16463  0nprm  16695  structcnvcnv  17170  fvsetsid  17185  fnpr2ob  17570  oduclatb  18515  0g0  18640  psgnunilem3  19475  zringndrg  21427  00ply1bas  22173  0ntop  22841  topnex  22932  bwth  23346  ustn0  24157  vitalilem5  25563  deg1nn0clb  26045  aaliou3lem9  26308  sinhalfpilem  26422  logdmn0  26599  dvlog  26610  ppiltx  27137  dchrisum0fno1  27472  nosgnn0i  27621  sltsolem1  27637  nolt02o  27657  nogt01o  27658  noprc  27741  oldirr  27845  leftirr  27846  rightirr  27847  axlowdim1  28884  topnfbey  30396  0ngrp  30438  dmadjrnb  31833  neldifpr1  32460  neldifpr2  32461  1nei  32660  nn0xmulclb  32694  ballotlem2  34467  bnj1304  34796  bnj110  34835  bnj98  34844  bnj1523  35048  subfacp1lem5  35152  msrrcl  35511  linedegen  36107  rankeq1o  36135  neufal  36370  neutru  36371  unqsym1  36389  onpsstopbas  36394  ordcmp  36411  onint1  36413  bj-ru  36908  bj-1nel0  36918  bj-0nelsngl  36935  bj-0nmoore  37076  bj-ccinftydisj  37177  relowlpssretop  37328  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem30  37620  zrdivrng  37923  prtlem400  38834  equidqe  38886  sn-inelr  42457  eldioph4b  42781  jm2.23  42967  ttac  43007  sucomisnotcard  43515  clsk1indlem1  44016  rusbcALT  44411  nimnbi  45135  nimnbi2  45136  fouriersw  46208  aibnbna  46883  dtrucor3  48726  fonex  48790