Theorem mto 196

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 193	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  200  mtbi  322  intnan  488  intnanr  489  pm3.2ni  880  nexr  2186  nonconne  2953  ru  3777  noelOLD  4332  reu0  4359  neldifsn  4796  axnulALT  5305  nvel  5317  nfnid  5374  nprrel  5736  0xp  5775  son2lpi  6130  nlim0  6424  snsn0non  6490  onnev  6492  nfunv  6582  dffv3  6888  mpo0  7494  onprc  7765  ordeleqon  7769  onuninsuci  7829  orduninsuc  7832  iprc  7904  poxp2  8129  poxp3  8136  tfrlem13  8390  tfrlem14  8391  tfrlem16  8393  tfr2b  8396  tz7.44lem1  8405  nlim1  8489  nlim2  8490  sdomn2lp  9116  canth2  9130  map2xp  9147  snnen2o  9237  1sdom2dom  9247  fi0  9415  sucprcreg  9596  rankxplim3  9876  alephnbtwn2  10067  alephprc  10094  unialeph  10096  kmlem16  10160  cfsuc  10252  nd1  10582  nd2  10583  canthp1lem2  10648  0nnq  10919  1ne0sr  11091  pnfnre  11255  mnfnre  11257  ine0  11649  recgt0ii  12120  inelr  12202  0nnn  12248  nnunb  12468  nn0nepnf  12552  indstr  12900  1nuz2  12908  0nrp  13009  lsw0  14515  egt2lt3  16149  ruc  16186  odd2np1  16284  divalglem5  16340  bitsf1  16387  0nprm  16615  structcnvcnv  17086  fvsetsid  17101  fnpr2ob  17504  oduclatb  18460  0g0  18583  psgnunilem3  19364  zringndrg  21038  00ply1bas  21762  0ntop  22407  topnex  22499  bwth  22914  ustn0  23725  vitalilem5  25129  deg1nn0clb  25608  aaliou3lem9  25863  sinhalfpilem  25973  logdmn0  26148  dvlog  26159  ppiltx  26681  dchrisum0fno1  27014  nosgnn0i  27162  sltsolem1  27178  nolt02o  27198  nogt01o  27199  noprc  27281  oldirr  27384  leftirr  27385  rightirr  27386  axlowdim1  28217  topnfbey  29722  0ngrp  29764  dmadjrnb  31159  neldifpr1  31770  neldifpr2  31771  1nei  31961  nn0xmulclb  31984  ballotlem2  33487  bnj1304  33830  bnj110  33869  bnj98  33878  bnj1523  34082  subfacp1lem5  34175  msrrcl  34534  linedegen  35115  rankeq1o  35143  neufal  35291  neutru  35292  unqsym1  35310  onpsstopbas  35315  ordcmp  35332  onint1  35334  bj-ru0  35823  bj-ru  35825  bj-1nel0  35835  bj-0nelsngl  35852  bj-0nmoore  35993  bj-ccinftydisj  36094  relowlpssretop  36245  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem30  36518  zrdivrng  36821  prtlem400  37740  equidqe  37792  sn-inelr  41338  eldioph4b  41549  jm2.23  41735  ttac  41775  sucomisnotcard  42295  clsk1indlem1  42796  rusbcALT  43198  nimnbi  43858  nimnbi2  43859  fouriersw  44947  aibnbna  45616  dtrucor3  47484