Theorem mto 198

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 157. (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 195	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  202  mtbi  323  intnan  487  intnanr  488  pm3.2ni  875  nexr  2154  nonconne  2995  ru  3706  noel  4218  reu0  4240  neldifsn  4634  axnulALT  5102  nvel  5114  nfnid  5170  nprrel  5500  0xp  5538  son2lpi  5867  nlim0  6127  snsn0non  6187  nfunv  6261  dffv3  6537  mpo0  7098  onprc  7358  ordeleqon  7362  onuninsuci  7414  orduninsuc  7417  iprc  7477  tfrlem13  7881  tfrlem14  7882  tfrlem16  7884  tfr2b  7887  tz7.44lem1  7896  sdomn2lp  8506  canth2  8520  map2xp  8537  fi0  8733  sucprcreg  8914  rankxplim3  9159  alephnbtwn2  9347  alephprc  9374  unialeph  9376  kmlem16  9440  cfsuc  9528  nd1  9858  nd2  9859  canthp1lem2  9924  0nnq  10195  1ne0sr  10367  pnfnre  10531  mnfnre  10533  ine0  10925  recgt0ii  11396  inelr  11478  0nnn  11523  nnunb  11743  nn0nepnf  11825  indstr  12165  1nuz2  12173  0nrp  12274  lsw0  13763  egt2lt3  15392  ruc  15429  odd2np1  15523  n2dvds1OLD  15551  divalglem5  15581  bitsf1  15628  0nprm  15851  structcnvcnv  16326  fvsetsid  16344  fnpr2ob  16660  oduclatb  17583  0g0  17702  psgnunilem3  18355  00ply1bas  20091  zringndrg  20319  0ntop  21197  topnex  21288  bwth  21702  ustn0  22512  vitalilem5  23896  deg1nn0clb  24367  aaliou3lem9  24622  sinhalfpilem  24732  logdmn0  24904  dvlog  24915  ppiltx  25436  dchrisum0fno1  25769  axlowdim1  26428  topnfbey  27931  0ngrp  27971  dmadjrnb  29366  neldifpr1  29974  neldifpr2  29975  1nei  30152  nn0xmulclb  30176  ballotlem2  31355  bnj521  31616  bnj1304  31700  bnj110  31738  bnj98  31747  bnj1523  31949  subfacp1lem5  32033  msrrcl  32392  nosgnn0i  32769  sltsolem1  32783  nolt02o  32802  noprc  32852  linedegen  33207  rankeq1o  33235  neufal  33357  neutru  33358  unqsym1  33376  amosym1  33377  onpsstopbas  33381  ordcmp  33398  onint1  33400  bj-ru0  33822  bj-ru  33824  bj-1nel0  33835  bj-0nelsngl  33901  bj-0nmoore  34017  bj-ccinftydisj  34066  relowlpssretop  34189  poimirlem16  34452  poimirlem17  34453  poimirlem18  34454  poimirlem19  34455  poimirlem20  34456  poimirlem22  34458  poimirlem30  34466  zrdivrng  34776  prtlem400  35550  equidqe  35602  nsb  38644  eldioph4b  38906  jm2.23  39091  ttac  39131  clsk1indlem1  39893  rusbcALT  40322  fouriersw  42072  aibnbna  42697