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  2938  ruOLD  3755  reu0  4327  neldifsn  4759  axnulALT  5262  nvel  5274  nfnid  5333  nprrel  5700  0xp  5740  son2lpi  6104  nlim0  6395  snsn0non  6462  onnev  6464  nfunv  6552  dffv3  6857  mpo0  7477  onprc  7757  ordeleqon  7761  onuninsuci  7819  orduninsuc  7822  iprc  7890  poxp2  8125  poxp3  8132  tfrlem13  8361  tfrlem14  8362  tfrlem16  8364  tfr2b  8367  tz7.44lem1  8376  nlim1  8456  nlim2  8457  sdomn2lp  9086  canth2  9100  map2xp  9117  snnen2o  9191  1sdom2dom  9201  fi0  9378  sucprcreg  9561  rankxplim3  9841  alephnbtwn2  10032  alephprc  10059  unialeph  10061  kmlem16  10126  cfsuc  10217  nd1  10547  nd2  10548  canthp1lem2  10613  0nnq  10884  1ne0sr  11056  pnfnre  11222  mnfnre  11224  ine0  11620  recgt0ii  12096  inelr  12183  0nnn  12229  nnunb  12445  nn0nepnf  12530  indstr  12882  1nuz2  12890  0nrp  12995  lsw0  14537  egt2lt3  16181  ruc  16218  odd2np1  16318  divalglem5  16374  bitsf1  16423  0nprm  16655  structcnvcnv  17130  fvsetsid  17145  fnpr2ob  17528  oduclatb  18473  0g0  18598  psgnunilem3  19433  zringndrg  21385  00ply1bas  22131  0ntop  22799  topnex  22890  bwth  23304  ustn0  24115  vitalilem5  25520  deg1nn0clb  26002  aaliou3lem9  26265  sinhalfpilem  26379  logdmn0  26556  dvlog  26567  ppiltx  27094  dchrisum0fno1  27429  nosgnn0i  27578  sltsolem1  27594  nolt02o  27614  nogt01o  27615  noprc  27698  oldirr  27808  leftirr  27809  rightirr  27810  axlowdim1  28893  topnfbey  30405  0ngrp  30447  dmadjrnb  31842  neldifpr1  32469  neldifpr2  32470  1nei  32667  nn0xmulclb  32701  cos9thpinconstr  33788  trisecnconstr  33789  ballotlem2  34487  bnj1304  34816  bnj110  34855  bnj98  34864  bnj1523  35068  subfacp1lem5  35178  msrrcl  35537  linedegen  36138  rankeq1o  36166  neufal  36401  neutru  36402  unqsym1  36420  onpsstopbas  36425  ordcmp  36442  onint1  36444  bj-ru  36939  bj-1nel0  36949  bj-0nelsngl  36966  bj-0nmoore  37107  bj-ccinftydisj  37208  relowlpssretop  37359  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem30  37651  zrdivrng  37954  prtlem400  38870  equidqe  38922  sn-inelr  42482  eldioph4b  42806  jm2.23  42992  ttac  43032  sucomisnotcard  43540  clsk1indlem1  44041  rusbcALT  44435  nimnbi  45164  nimnbi2  45165  fouriersw  46236  aibnbna  46911  dtrucor3  48791  fonex  48859