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  881  ru0  2133  nexr  2200  nonconne  2945  ruOLD  3741  reu0  4315  neldifsn  4750  axnulALT  5251  nvel  5263  nfnid  5322  nprrel  5691  0xp  5731  xp0  5732  son2lpi  6093  nlim0  6385  snsn0non  6451  onnev  6453  nfunv  6533  dffv3  6838  mpo0  7453  onprc  7733  ordeleqon  7737  onuninsuci  7792  orduninsuc  7795  iprc  7863  poxp2  8095  poxp3  8102  tfrlem13  8331  tfrlem14  8332  tfrlem16  8334  tfr2b  8337  tz7.44lem1  8346  nlim1  8426  nlim2  8427  sdomn2lp  9056  canth2  9070  map2xp  9087  ordfin  9152  snnen2o  9157  1sdom2dom  9166  fi0  9335  sucprcreg  9521  rankxplim3  9805  alephnbtwn2  9994  alephprc  10021  unialeph  10023  kmlem16  10088  cfsuc  10179  nd1  10510  nd2  10511  canthp1lem2  10576  0nnq  10847  1ne0sr  11019  pnfnre  11185  mnfnre  11187  ine0  11584  recgt0ii  12060  inelr  12147  0nnn  12193  nnunb  12409  nn0nepnf  12494  indstr  12841  1nuz2  12849  0nrp  12954  lsw0  14500  egt2lt3  16143  ruc  16180  odd2np1  16280  divalglem5  16336  bitsf1  16385  0nprm  16617  structcnvcnv  17092  fvsetsid  17107  fnpr2ob  17491  oduclatb  18442  0g0  18601  psgnunilem3  19437  zringndrg  21435  00ply1bas  22192  0ntop  22861  topnex  22952  bwth  23366  ustn0  24177  vitalilem5  25581  deg1nn0clb  26063  aaliou3lem9  26326  sinhalfpilem  26440  logdmn0  26617  dvlog  26628  ppiltx  27155  dchrisum0fno1  27490  nosgnn0i  27639  ltssolem1  27655  nolt02o  27675  nogt01o  27676  noprc  27764  oldirr  27898  leftirr  27899  rightirr  27900  axlowdim1  29044  topnfbey  30556  nowisdomv  30561  0ngrp  30599  dmadjrnb  31994  neldifpr1  32620  neldifpr2  32621  1nei  32827  nn0xmulclb  32862  gsummulsubdishift1  33162  ply1coedeg  33682  cos9thpinconstr  33969  trisecnconstr  33970  ballotlem2  34667  bnj1304  34995  bnj110  35034  bnj98  35043  bnj1523  35247  axnulALT2  35258  fineqvinfep  35303  subfacp1lem5  35400  msrrcl  35759  linedegen  36359  rankeq1o  36387  neufal  36622  neutru  36623  unqsym1  36641  onpsstopbas  36646  ordcmp  36663  onint1  36665  bj-ru  37192  bj-1nel0  37202  bj-0nelsngl  37219  bj-0nmoore  37365  bj-ccinftydisj  37468  relowlpssretop  37619  poimirlem16  37887  poimirlem17  37888  poimirlem18  37889  poimirlem19  37890  poimirlem20  37891  poimirlem22  37893  poimirlem30  37901  zrdivrng  38204  prtlem400  39246  equidqe  39298  sn-inelr  42857  eldioph4b  43168  jm2.23  43353  ttac  43393  sucomisnotcard  43900  clsk1indlem1  44401  rusbcALT  44794  nimnbi  45522  nimnbi2  45523  fouriersw  46589  nthrucw  47244  cjnpoly  47249  tannpoly  47250  sinnpoly  47251  aibnbna  47266  dtrucor3  49158  fonex  49226