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  2124  nexr  2189  nonconne  2949  ruOLD  3789  reu0  4366  neldifsn  4796  axnulALT  5309  nvel  5321  nfnid  5380  nprrel  5747  0xp  5786  son2lpi  6150  nlim0  6444  snsn0non  6510  onnev  6512  nfunv  6600  dffv3  6902  mpo0  7517  onprc  7796  ordeleqon  7800  onuninsuci  7860  orduninsuc  7863  iprc  7933  poxp2  8166  poxp3  8173  tfrlem13  8428  tfrlem14  8429  tfrlem16  8431  tfr2b  8434  tz7.44lem1  8443  nlim1  8525  nlim2  8526  sdomn2lp  9154  canth2  9168  map2xp  9185  snnen2o  9270  1sdom2dom  9280  fi0  9457  sucprcreg  9638  rankxplim3  9918  alephnbtwn2  10109  alephprc  10136  unialeph  10138  kmlem16  10203  cfsuc  10294  nd1  10624  nd2  10625  canthp1lem2  10690  0nnq  10961  1ne0sr  11133  pnfnre  11299  mnfnre  11301  ine0  11695  recgt0ii  12171  inelr  12253  0nnn  12299  nnunb  12519  nn0nepnf  12604  indstr  12955  1nuz2  12963  0nrp  13067  lsw0  14599  egt2lt3  16238  ruc  16275  odd2np1  16374  divalglem5  16430  bitsf1  16479  0nprm  16711  structcnvcnv  17186  fvsetsid  17201  fnpr2ob  17604  oduclatb  18564  0g0  18689  psgnunilem3  19528  zringndrg  21496  00ply1bas  22256  0ntop  22926  topnex  23018  bwth  23433  ustn0  24244  vitalilem5  25660  deg1nn0clb  26143  aaliou3lem9  26406  sinhalfpilem  26519  logdmn0  26696  dvlog  26707  ppiltx  27234  dchrisum0fno1  27569  nosgnn0i  27718  sltsolem1  27734  nolt02o  27754  nogt01o  27755  noprc  27838  oldirr  27942  leftirr  27943  rightirr  27944  axlowdim1  28988  topnfbey  30497  0ngrp  30539  dmadjrnb  31934  neldifpr1  32558  neldifpr2  32559  1nei  32753  nn0xmulclb  32781  ballotlem2  34469  bnj1304  34811  bnj110  34850  bnj98  34859  bnj1523  35063  subfacp1lem5  35168  msrrcl  35527  linedegen  36124  rankeq1o  36152  neufal  36388  neutru  36389  unqsym1  36407  onpsstopbas  36412  ordcmp  36429  onint1  36431  bj-ru  36926  bj-1nel0  36936  bj-0nelsngl  36953  bj-0nmoore  37094  bj-ccinftydisj  37195  relowlpssretop  37346  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem30  37636  zrdivrng  37939  prtlem400  38851  equidqe  38903  sn-inelr  42473  eldioph4b  42798  jm2.23  42984  ttac  43024  sucomisnotcard  43533  clsk1indlem1  44034  rusbcALT  44434  nimnbi  45105  nimnbi2  45106  fouriersw  46186  aibnbna  46855  dtrucor3  48647