Theorem mto 188

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 150. (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 185	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  192  mtbi  312  pm3.2ni  899  intnan  960  intnanr  961  nexr  2062  nonconne  2806  ru  3434  neldifsn  4321  axnulALT  4787  nvel  4797  nfnid  4897  nprrel  5161  0xp  5199  son2lpi  5524  nlim0  5783  snsn0non  5846  nfunv  5921  dffv3  6187  mpt20  6725  snnexOLD  6967  onprc  6984  ordeleqon  6988  onuninsuci  7040  orduninsuc  7043  iprc  7101  tfrlem13  7486  tfrlem14  7487  tfrlem16  7489  tfr2b  7492  tz7.44lem1  7501  sdomn2lp  8099  canth2  8113  map2xp  8130  fi0  8326  sucprcreg  8506  rankxplim3  8744  alephnbtwn2  8895  alephprc  8922  unialeph  8924  kmlem16  8987  cfsuc  9079  nd1  9409  nd2  9410  canthp1lem2  9475  0nnq  9746  1ne0sr  9917  pnfnre  10081  mnfnre  10082  ine0  10465  recgt0ii  10929  inelr  11010  nnunb  11288  nn0nepnf  11371  indstr  11756  1nuz2  11764  0nrp  11865  zgt1rpn0n1  11871  lsw0  13352  egt2lt3  14934  ruc  14972  odd2np1  15065  n2dvds1  15104  divalglem5  15120  bitsf1  15168  structcnvcnv  15871  fvsetsid  15890  strlemor1OLD  15969  meet0  17137  join0  17138  oduclatb  17144  0g0  17263  psgnunilem3  17916  00ply1bas  19610  zringndrg  19838  0ntop  20710  topnex  20800  bwth  21213  ustn0  22024  vitalilem5  23381  deg1nn0clb  23850  aaliou3lem9  24105  sinhalfpilem  24215  logdmn0  24386  dvlog  24397  ppiltx  24903  dchrisum0fno1  25200  axlowdim1  25839  topnfbey  27325  0ngrp  27365  dmadjrnb  28765  ballotlem2  30550  bnj521  30805  bnj1304  30890  bnj110  30928  bnj98  30937  bnj1523  31139  subfacp1lem5  31166  msrrcl  31440  nosgnn0i  31812  sltsolem1  31826  nolt02o  31845  noprc  31895  linedegen  32250  rankeq1o  32278  unnf  32406  unnt  32407  unqsym1  32424  amosym1  32425  onpsstopbas  32429  ordcmp  32446  onint1  32448  bj-babygodel  32588  bj-ru0  32932  bj-ru  32934  bj-1nel0  32941  bj-0nelsngl  32959  bj-0nmoore  33067  bj-ccinftydisj  33100  relowlpssretop  33212  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem30  33439  zrdivrng  33752  prtlem400  34155  equidqe  34207  eldioph4b  37375  jm2.23  37563  ttac  37603  clsk1indlem1  38343  rusbcALT  38640  fouriersw  40448  aibnbna  41073