Theorem 3eqtr3rd 2810

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

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
2		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtr3d 2803	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2803	1 ⊢ (𝜑 → 𝐷 = 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758

This theorem is used by:  iunxdif3  5066  fcofo  7297  fcof1oinvd  7302  cantnfp1lem3  9659  fin1a2lem7  10408  prlem934  11036  addlid  11411  addcom  11414  addcomd  11430  negeu  11465  add20  11744  2halves  12480  bcnn  14368  bcpasc  14377  hashfun  14494  hashf1dmrn  14500  ccatf1  14648  wrdeqs1cat  14781  sqreulem  15437  summolem3  15791  fsumneg  15864  geolim  15950  geolim2  15951  mertens  15966  prodmolem3  16013  fallrisefac  16105  bpoly3  16137  sincossq  16257  demoivre  16281  eirrlem  16285  oddpwp1fsum  16475  sadeq  16555  gcdid  16610  gcdmultipled  16617  nn0rppwr  16644  phiprmpw  16860  pythagtriplem12  16911  expnprm  16987  fullresc  17933  grpinvid1  19089  grpnpcan  19129  grplactcnv  19140  ghmgrp  19163  qustrivr  19284  conjghm  19350  odmodnn0  19641  gex1  19692  sylow3lem3  19730  efgredeu  19853  odadd2  19950  gsumval3  20008  pgpfac1lem3a  20179  omndmul2  20234  ringnegl  20418  ringnegr  20419  ringmneg2  20421  rdivmuldivd  20528  imadrhmcl  20937  lmodfopne  21058  lmodvsneg  21064  lssvs0or  21271  lvecinv  21274  lspabs2  21281  zringunit  21653  zringcyg  21656  dvdschrmulg  21715  fermltlchr  21716  sraassab  22055  mplcoe3  22226  mplcoe5  22228  evlvar  22296  psd1  22367  mdetrlin  22796  mdetunilem6  22811  cramerimplem3  22879  cramerimp  22880  paste  23488  tuslem  24460  tususs  24463  ngpds  24798  ioo2bl  24987  ipcau2  25430  dvexp3  26174  rolle  26186  cmvth  26187  dv11cn  26197  lhop  26212  itgsubstlem  26244  itgpowd  26246  ply1divex  26331  fta1glem1  26362  fta1g  26364  dgrnznn  26441  fta1  26506  vieta1lem2  26509  aaliou2  26540  dvtaylp  26570  dvntaylp  26571  taylthlem1  26573  taylthlem2  26574  dvradcnv  26621  ptolemy  26698  coskpi  26725  tanregt0  26741  cxpeq  26959  isosctrlem2  27021  chordthmlem  27034  dcubic  27048  quart1lem  27057  tanatan  27121  atantan  27125  dvatan  27137  birthdaylem2  27154  rlimcxp  27175  jensenlem2  27189  logdiflbnd  27196  emcllem2  27198  lgamgulmlem2  27231  lgamcvg2  27256  basellem8  27289  bclbnd  27481  lgsqr  27552  lgseisenlem3  27578  lgseisenlem4  27579  lgsquadlem1  27581  lgsquadlem2  27582  rpvmasumlem  27688  dchrisumlem1  27690  dchrisum0flblem1  27709  dchrisum0flblem2  27710  dchrisum0re  27714  dchrisum0lem1  27717  mudivsum  27731  mulogsum  27733  vmalogdivsum2  27739  logsqvma2  27744  selberg2lem  27751  logdivbnd  27757  selbergr  27769  selberg3r  27770  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  pntpbnd2  27788  pw2divscan4d  28674  pw2cutp1  28691  pw2cut2  28692  z12zsodd  28712  miduniq  28999  krippenlem  29004  colperpexlem2  29049  plngrotlem1  29106  ttgcontlem1  29271  brbtwn2  29292  colinearalglem4  29296  axsegconlem9  29312  ax5seglem1  29315  axbtwnid  29326  axeuclidlem  29349  axcontlem2  29352  axcontlem4  29354  grpoinvid1  30917  vcz  30964  hosubsub4  32207  lnop0  32355  branmfn  32494  fressupp  33070  difico  33165  wrdsplex  33293  s3f1  33301  mgcf1o  33354  mndlrinv  33375  cycpmco2lem4  33480  tocyccntz  33495  cyc3genpm  33503  cycpmconjslem2  33506  rlocisunit  33627  kerunit  33676  znfermltl  33712  linds2eq  33725  dvdsruassoi  33728  dvdsruasso  33729  qsdrnglem2  33809  zringfrac  33875  m1pmeq  33906  vr1nz  33914  mplvrpmrhm  33968  esplyfval1  33994  ply1degltdimlem  34043  fedgmullem2  34051  fldextrspunlsplem  34094  constrrtll  34152  constrrtlc1  34153  constrrtcclem  34155  constrrtcc  34156  constrrecl  34190  2sqr3minply  34201  cos9thpiminplylem1  34203  cos9thpiminplylem2  34204  carsggect  34739  carsgclctunlem2  34740  ballotlemfrceq  34950  ballotlemrinv0  34954  hashreprin  35038  hgt750lemb  35074  faclimlem1  36255  irrdifflemf  38009  poimirlem4  38315  poimirlem23  38334  mblfinlem2  38349  voliunnfl  38355  volsupnfl  38356  itg2addnclem3  38364  ftc2nc  38393  dvasin  38395  areacirclem1  38399  areacirclem4  38402  rngonegmn1l  38632  rngonegmn1r  38633  lfl0  39879  latmassOLD  40043  omlmod1i2N  40074  llnexchb2lem  40682  dalawlem3  40687  pmapj2N  40743  osumcllem9N  40778  pexmidlem6N  40789  4atexlemc  40883  cdleme1  41041  cdleme42a  41285  cdlemg13a  41465  cdlemh2  41630  cdlemk1  41645  tendocnv  41835  dihmeetlem12N  42132  dihmeetlem16N  42136  dihmeetlem19N  42139  dochsatshp  42265  dochexmidlem6  42279  mapdval4N  42446  mapdpglem28  42515  mapdpglem31  42517  mapdindp4  42537  hdmap14lem1a  42680  hdmapinvlem4  42735  3rdpwhole  43093  oexpreposd  43123  remul01  43208  sn-negex12  43218  sn-subeu  43228  remulinvcom  43234  sn-0tie0  43265  cnreeu  43304  fltnlta  43435  irrapxlem5  43593  pellfund14  43665  rmxdbl  43706  jm2.22  43762  oaabsb  44061  oaun2  44148  oaun3  44149  sqrtcval  44407  0ellimcdiv  46403  fourierdlem95  46955  etransclem46  47034  sigariz  47617  sin5tlem2  47651  sin5tlem5  47654  cos5t  47656  ichreuopeq  48262  gricushgr  48722  altgsumbc  49172  blengt1fldiv2p1  49413  restclsseplem  49733  cofu1a  49912  cofu2a  49913  uobeqw  50037  swapf2fval  50083  swapf1val  50085  coccom  50482