MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr3rd Structured version   Visualization version   GIF version

Theorem 3eqtr3rd 2845
Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
Hypotheses
Ref Expression
3eqtr3d.1 (𝜑𝐴 = 𝐵)
3eqtr3d.2 (𝜑𝐴 = 𝐶)
3eqtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eqtr3rd (𝜑𝐷 = 𝐶)

Proof of Theorem 3eqtr3rd
StepHypRef Expression
1 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
2 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
3 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
42, 3eqtr3d 2838 . 2 (𝜑𝐵 = 𝐶)
51, 4eqtr3d 2838 1 (𝜑𝐷 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794
This theorem is referenced by:  iunxdif3  4983  fcofo  7026  fcof1oinvd  7031  cantnfp1lem3  9131  fin1a2lem7  9821  prlem934  10448  addid2  10816  addcom  10819  addcomd  10835  negeu  10869  add20  11145  2halves  11857  bcnn  13672  bcpasc  13681  hashfun  13798  wrdeqs1cat  14077  sqreulem  14715  summolem3  15067  fsumneg  15138  geolim  15222  geolim2  15223  mertens  15238  prodmolem3  15283  fallrisefac  15375  bpoly3  15408  sincossq  15525  demoivre  15549  eirrlem  15553  oddpwp1fsum  15737  sadeq  15815  gcdid  15869  gcdmultipled  15876  phiprmpw  16107  pythagtriplem12  16157  expnprm  16232  fullresc  17117  grpinvid1  18150  grpnpcan  18187  grplactcnv  18198  ghmgrp  18219  conjghm  18385  odmodnn0  18664  gex1  18712  sylow3lem3  18750  efgredeu  18874  odadd2  18966  gsumval3  19024  pgpfac1lem3a  19195  ringnegl  19344  rngnegr  19345  ringmneg2  19347  lmodfopne  19669  lmodvsneg  19675  lss0v  19785  lssvs0or  19879  lvecinv  19882  lspabs2  19889  zringunit  20185  zringcyg  20188  mplcoe3  20710  mplcoe5  20712  evlvar  20776  mdetrlin  21211  mdetunilem6  21226  cramerimplem3  21294  cramerimp  21295  paste  21903  tuslem  22877  tususs  22880  ngpds  23214  ioo2bl  23402  ipcau2  23842  dvexp3  24585  rolle  24597  cmvth  24598  dv11cn  24608  lhop  24623  itgsubstlem  24655  itgpowd  24657  ply1divex  24741  fta1glem1  24770  fta1g  24772  dgrnznn  24848  fta1  24908  vieta1lem2  24911  aaliou2  24940  dvtaylp  24969  dvntaylp  24970  taylthlem1  24972  taylthlem2  24973  dvradcnv  25020  ptolemy  25093  coskpi  25119  tanregt0  25135  cxpeq  25350  isosctrlem2  25409  chordthmlem  25422  dcubic  25436  quart1lem  25445  tanatan  25509  atantan  25513  dvatan  25525  birthdaylem2  25542  rlimcxp  25563  jensenlem2  25577  logdiflbnd  25584  emcllem2  25586  lgamgulmlem2  25619  lgamcvg2  25644  basellem8  25677  bclbnd  25868  lgsqr  25939  lgseisenlem3  25965  lgseisenlem4  25966  lgsquadlem1  25968  lgsquadlem2  25969  rpvmasumlem  26075  dchrisumlem1  26077  dchrisum0flblem1  26096  dchrisum0flblem2  26097  dchrisum0re  26101  dchrisum0lem1  26104  mudivsum  26118  mulogsum  26120  vmalogdivsum2  26126  logsqvma2  26131  selberg2lem  26138  logdivbnd  26144  selbergr  26156  selberg3r  26157  pntrlog2bndlem4  26168  pntrlog2bndlem5  26169  pntpbnd2  26175  miduniq  26483  krippenlem  26488  colperpexlem2  26529  ttgcontlem1  26683  brbtwn2  26703  colinearalglem4  26707  axsegconlem9  26723  ax5seglem1  26726  axbtwnid  26737  axeuclidlem  26760  axcontlem2  26763  axcontlem4  26765  grpoinvid1  28315  vcz  28362  hosubsub4  29605  lnop0  29753  branmfn  29892  fressupp  30452  difico  30536  wrdsplex  30644  s3f1  30653  ccatf1  30655  omndmul2  30767  cycpmco2lem4  30825  tocyccntz  30840  cyc3genpm  30848  cycpmconjslem2  30851  dvdschrmulg  30912  rdivmuldivd  30917  kerunit  30951  qustrivr  30985  linds2eq  30999  fedgmullem2  31118  carsggect  31690  carsgclctunlem2  31691  ballotlemfrceq  31900  ballotlemrinv0  31904  hashreprin  32005  hgt750lemb  32041  hashf1dmrn  32469  faclimlem1  33089  irrdifflemf  34740  poimirlem4  35060  poimirlem23  35079  mblfinlem2  35094  voliunnfl  35100  volsupnfl  35101  itg2addnclem3  35109  ftc2nc  35138  dvasin  35140  areacirclem1  35144  areacirclem4  35147  rngonegmn1l  35378  rngonegmn1r  35379  lfl0  36360  latmassOLD  36524  omlmod1i2N  36555  llnexchb2lem  37163  dalawlem3  37168  pmapj2N  37224  osumcllem9N  37259  pexmidlem6N  37270  4atexlemc  37364  cdleme1  37522  cdleme42a  37766  cdlemg13a  37946  cdlemh2  38111  cdlemk1  38126  tendocnv  38316  dihmeetlem12N  38613  dihmeetlem16N  38617  dihmeetlem19N  38620  dochsatshp  38746  dochexmidlem6  38760  mapdval4N  38927  mapdpglem28  38996  mapdpglem31  38998  mapdindp4  39018  hdmap14lem1a  39161  hdmapinvlem4  39216  oexpreposd  39484  nn0rppwr  39487  sn-00idlem3  39535  remul01  39542  sn-subeu  39560  remulinvcom  39566  sn-0tie0  39573  cnreeu  39590  fltnlta  39616  irrapxlem5  39764  pellfund14  39836  rmxdbl  39877  jm2.22  39933  sqrtcval  40338  0ellimcdiv  42288  fourierdlem95  42840  etransclem46  42919  sigariz  43474  ichreuopeq  43987  isomushgr  44341  altgsumbc  44751  blengt1fldiv2p1  45004
  Copyright terms: Public domain W3C validator