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  311  pm3.2ni  935  intnan  998  intnanr  999  nexr  2209  nonconne  2944  ru  3575  neldifsn  4467  axnulALT  4939  nvel  4949  nfnid  5046  nprrel  5318  0xp  5356  son2lpi  5682  nlim0  5944  snsn0non  6007  nfunv  6082  dffv3  6348  mpt20  6890  snnexOLD  7132  onprc  7149  ordeleqon  7153  onuninsuci  7205  orduninsuc  7208  iprc  7266  tfrlem13  7655  tfrlem14  7656  tfrlem16  7658  tfr2b  7661  tz7.44lem1  7670  sdomn2lp  8264  canth2  8278  map2xp  8295  fi0  8491  sucprcreg  8671  rankxplim3  8917  alephnbtwn2  9085  alephprc  9112  unialeph  9114  kmlem16  9179  cfsuc  9271  nd1  9601  nd2  9602  canthp1lem2  9667  0nnq  9938  1ne0sr  10109  pnfnre  10273  mnfnre  10274  ine0  10657  recgt0ii  11121  inelr  11202  nnunb  11480  nn0nepnf  11563  indstr  11949  1nuz2  11957  0nrp  12058  zgt1rpn0n1  12064  lsw0  13539  egt2lt3  15133  ruc  15171  odd2np1  15267  n2dvds1  15306  divalglem5  15322  bitsf1  15370  structcnvcnv  16073  fvsetsid  16092  strlemor1OLD  16171  meet0  17338  join0  17339  oduclatb  17345  0g0  17464  psgnunilem3  18116  00ply1bas  19812  zringndrg  20040  0ntop  20912  topnex  21002  bwth  21415  ustn0  22225  vitalilem5  23580  deg1nn0clb  24049  aaliou3lem9  24304  sinhalfpilem  24414  logdmn0  24585  dvlog  24596  ppiltx  25102  dchrisum0fno1  25399  axlowdim1  26038  topnfbey  27636  0ngrp  27674  dmadjrnb  29074  ballotlem2  30859  bnj521  31112  bnj1304  31197  bnj110  31235  bnj98  31244  bnj1523  31446  subfacp1lem5  31473  msrrcl  31747  nosgnn0i  32118  sltsolem1  32132  nolt02o  32151  noprc  32201  linedegen  32556  rankeq1o  32584  unnf  32712  unnt  32713  unqsym1  32730  amosym1  32731  onpsstopbas  32735  ordcmp  32752  onint1  32754  bj-babygodel  32894  bj-ru0  33238  bj-ru  33240  bj-1nel0  33247  bj-0nelsngl  33265  bj-0nmoore  33373  bj-ccinftydisj  33411  relowlpssretop  33523  poimirlem16  33738  poimirlem17  33739  poimirlem18  33740  poimirlem19  33741  poimirlem20  33742  poimirlem22  33744  poimirlem30  33752  zrdivrng  34065  prtlem400  34659  equidqe  34711  eldioph4b  37877  jm2.23  38065  ttac  38105  clsk1indlem1  38845  rusbcALT  39142  fouriersw  40951  aibnbna  41579