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  898  intnan  959  intnanr  960  nexr  2060  nonconne  2802  ru  3421  neldifsn  4297  axnulALT  4757  nvel  4767  nfnid  4867  nprrel  5131  0xp  5170  son2lpi  5493  nlim0  5752  snsn0non  5815  nfunv  5889  dffv3  6154  mpt20  6690  snnexOLD  6931  onprc  6946  ordeleqon  6950  onuninsuci  7002  orduninsuc  7005  iprc  7063  tfrlem13  7446  tfrlem14  7447  tfrlem16  7449  tfr2b  7452  tz7.44lem1  7461  sdomn2lp  8059  canth2  8073  map2xp  8090  fi0  8286  sucprcreg  8466  rankxplim3  8704  alephnbtwn2  8855  alephprc  8882  unialeph  8884  kmlem16  8947  cfsuc  9039  nd1  9369  nd2  9370  canthp1lem2  9435  0nnq  9706  1ne0sr  9877  pnfnre  10041  mnfnre  10042  ine0  10425  recgt0ii  10889  inelr  10970  nnunb  11248  nn0nepnf  11331  indstr  11716  1nuz2  11724  0nrp  11825  zgt1rpn0n1  11831  lsw0  13307  egt2lt3  14878  ruc  14916  odd2np1  15008  n2dvds1  15047  divalglem5  15063  bitsf1  15111  structcnvcnv  15813  fvsetsid  15830  strlemor1OLD  15909  meet0  17077  join0  17078  oduclatb  17084  0g0  17203  psgnunilem3  17856  00ply1bas  19550  zringndrg  19778  0ntop  20650  topnex  20740  bwth  21153  ustn0  21964  vitalilem5  23321  deg1nn0clb  23788  aaliou3lem9  24043  sinhalfpilem  24153  logdmn0  24320  dvlog  24331  ppiltx  24837  dchrisum0fno1  25134  axlowdim1  25773  topnfbey  27213  0ngrp  27253  dmadjrnb  28653  ballotlem2  30373  bnj521  30566  bnj1304  30651  bnj110  30689  bnj98  30698  bnj1523  30900  subfacp1lem5  30927  msrrcl  31201  nosgnn0i  31566  sltsolem1  31581  noprc  31597  linedegen  31945  rankeq1o  31973  unnf  32101  unnt  32102  unqsym1  32119  amosym1  32120  onpsstopbas  32124  ordcmp  32141  onint1  32143  bj-babygodel  32283  bj-ru0  32632  bj-ru  32634  bj-1nel0  32641  bj-0nelsngl  32659  bj-ccinftydisj  32772  relowlpssretop  32883  poimirlem16  33096  poimirlem17  33097  poimirlem18  33098  poimirlem19  33099  poimirlem20  33100  poimirlem22  33102  poimirlem30  33110  zrdivrng  33423  prtlem400  33674  equidqe  33726  eldioph4b  36894  jm2.23  37082  ttac  37122  clsk1indlem1  37864  rusbcALT  38161  fouriersw  39785  aibnbna  40407