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  879  ru0  2127  nexr  2193  nonconne  2958  ruOLD  3803  noelOLD  4361  reu0  4384  neldifsn  4817  axnulALT  5322  nvel  5334  nfnid  5393  nprrel  5759  0xp  5798  son2lpi  6160  nlim0  6454  snsn0non  6520  onnev  6522  nfunv  6611  dffv3  6916  mpo0  7535  onprc  7813  ordeleqon  7817  onuninsuci  7877  orduninsuc  7880  iprc  7951  poxp2  8184  poxp3  8191  tfrlem13  8446  tfrlem14  8447  tfrlem16  8449  tfr2b  8452  tz7.44lem1  8461  nlim1  8545  nlim2  8546  sdomn2lp  9182  canth2  9196  map2xp  9213  snnen2o  9300  1sdom2dom  9310  fi0  9489  sucprcreg  9670  rankxplim3  9950  alephnbtwn2  10141  alephprc  10168  unialeph  10170  kmlem16  10235  cfsuc  10326  nd1  10656  nd2  10657  canthp1lem2  10722  0nnq  10993  1ne0sr  11165  pnfnre  11331  mnfnre  11333  ine0  11725  recgt0ii  12201  inelr  12283  0nnn  12329  nnunb  12549  nn0nepnf  12633  indstr  12981  1nuz2  12989  0nrp  13092  lsw0  14613  egt2lt3  16254  ruc  16291  odd2np1  16389  divalglem5  16445  bitsf1  16492  0nprm  16725  structcnvcnv  17200  fvsetsid  17215  fnpr2ob  17618  oduclatb  18577  0g0  18702  psgnunilem3  19538  zringndrg  21502  00ply1bas  22262  0ntop  22932  topnex  23024  bwth  23439  ustn0  24250  vitalilem5  25666  deg1nn0clb  26149  aaliou3lem9  26410  sinhalfpilem  26523  logdmn0  26700  dvlog  26711  ppiltx  27238  dchrisum0fno1  27573  nosgnn0i  27722  sltsolem1  27738  nolt02o  27758  nogt01o  27759  noprc  27842  oldirr  27946  leftirr  27947  rightirr  27948  axlowdim1  28992  topnfbey  30501  0ngrp  30543  dmadjrnb  31938  neldifpr1  32561  neldifpr2  32562  1nei  32750  nn0xmulclb  32778  ballotlem2  34453  bnj1304  34795  bnj110  34834  bnj98  34843  bnj1523  35047  subfacp1lem5  35152  msrrcl  35511  linedegen  36107  rankeq1o  36135  neufal  36372  neutru  36373  unqsym1  36391  onpsstopbas  36396  ordcmp  36413  onint1  36415  bj-ru  36910  bj-1nel0  36920  bj-0nelsngl  36937  bj-0nmoore  37078  bj-ccinftydisj  37179  relowlpssretop  37330  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem30  37610  zrdivrng  37913  prtlem400  38826  equidqe  38878  sn-inelr  42443  eldioph4b  42767  jm2.23  42953  ttac  42993  sucomisnotcard  43506  clsk1indlem1  44007  rusbcALT  44408  nimnbi  45069  nimnbi2  45070  fouriersw  46152  aibnbna  46821  dtrucor3  48532