Theorem 3eqtr3rd 2774

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 2767	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2767	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  iunxdif3  5062  fcofo  7266  fcof1oinvd  7271  cantnfp1lem3  9640  fin1a2lem7  10366  prlem934  10993  addlid  11364  addcom  11367  addcomd  11383  negeu  11418  add20  11697  2halves  12407  bcnn  14284  bcpasc  14293  hashfun  14409  hashf1dmrn  14415  wrdeqs1cat  14692  sqreulem  15333  summolem3  15687  fsumneg  15760  geolim  15843  geolim2  15844  mertens  15859  prodmolem3  15906  fallrisefac  15998  bpoly3  16031  sincossq  16151  demoivre  16175  eirrlem  16179  oddpwp1fsum  16369  sadeq  16449  gcdid  16504  gcdmultipled  16511  nn0rppwr  16538  phiprmpw  16753  pythagtriplem12  16804  expnprm  16880  fullresc  17820  grpinvid1  18930  grpnpcan  18971  grplactcnv  18982  ghmgrp  19005  conjghm  19188  odmodnn0  19477  gex1  19528  sylow3lem3  19566  efgredeu  19689  odadd2  19786  gsumval3  19844  pgpfac1lem3a  20015  ringnegl  20218  ringnegr  20219  ringmneg2  20221  rdivmuldivd  20329  imadrhmcl  20713  lmodfopne  20813  lmodvsneg  20819  lssvs0or  21027  lvecinv  21030  lspabs2  21037  zringunit  21383  zringcyg  21386  dvdschrmulg  21445  fermltlchr  21446  sraassab  21784  mplcoe3  21952  mplcoe5  21954  evlvar  22014  psd1  22061  mdetrlin  22496  mdetunilem6  22511  cramerimplem3  22579  cramerimp  22580  paste  23188  tuslem  24161  tususs  24164  ngpds  24499  ioo2bl  24688  ipcau2  25141  dvexp3  25889  rolle  25901  cmvth  25902  cmvthOLD  25903  dv11cn  25913  lhop  25928  itgsubstlem  25962  itgpowd  25964  ply1divex  26049  fta1glem1  26080  fta1g  26082  dgrnznn  26159  fta1  26223  vieta1lem2  26226  aaliou2  26255  dvtaylp  26285  dvntaylp  26286  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  dvradcnv  26337  ptolemy  26412  coskpi  26439  tanregt0  26455  cxpeq  26674  isosctrlem2  26736  chordthmlem  26749  dcubic  26763  quart1lem  26772  tanatan  26836  atantan  26840  dvatan  26852  birthdaylem2  26869  rlimcxp  26891  jensenlem2  26905  logdiflbnd  26912  emcllem2  26914  lgamgulmlem2  26947  lgamcvg2  26972  basellem8  27005  bclbnd  27198  lgsqr  27269  lgseisenlem3  27295  lgseisenlem4  27296  lgsquadlem1  27298  lgsquadlem2  27299  rpvmasumlem  27405  dchrisumlem1  27407  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0re  27431  dchrisum0lem1  27434  mudivsum  27448  mulogsum  27450  vmalogdivsum2  27456  logsqvma2  27461  selberg2lem  27468  logdivbnd  27474  selbergr  27486  selberg3r  27487  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntpbnd2  27505  pw2cutp1  28343  miduniq  28619  krippenlem  28624  colperpexlem2  28665  ttgcontlem1  28819  brbtwn2  28839  colinearalglem4  28843  axsegconlem9  28859  ax5seglem1  28862  axbtwnid  28873  axeuclidlem  28896  axcontlem2  28899  axcontlem4  28901  grpoinvid1  30464  vcz  30511  hosubsub4  31754  lnop0  31902  branmfn  32041  fressupp  32618  difico  32713  wrdsplex  32864  s3f1  32875  ccatf1  32877  mgcf1o  32936  mndlrinv  32972  omndmul2  33033  cycpmco2lem4  33093  tocyccntz  33108  cyc3genpm  33116  cycpmconjslem2  33119  kerunit  33304  qustrivr  33343  znfermltl  33344  linds2eq  33359  dvdsruassoi  33362  dvdsruasso  33363  qsdrnglem2  33474  zringfrac  33532  m1pmeq  33559  vr1nz  33566  ply1degltdimlem  33625  fedgmullem2  33633  fldextrspunlsplem  33675  constrrtll  33728  constrrtlc1  33729  constrrtcclem  33731  constrrtcc  33732  constrrecl  33766  2sqr3minply  33777  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  carsggect  34316  carsgclctunlem2  34317  ballotlemfrceq  34527  ballotlemrinv0  34531  hashreprin  34618  hgt750lemb  34654  faclimlem1  35737  irrdifflemf  37320  poimirlem4  37625  poimirlem23  37644  mblfinlem2  37659  voliunnfl  37665  volsupnfl  37666  itg2addnclem3  37674  ftc2nc  37703  dvasin  37705  areacirclem1  37709  areacirclem4  37712  rngonegmn1l  37942  rngonegmn1r  37943  lfl0  39065  latmassOLD  39229  omlmod1i2N  39260  llnexchb2lem  39869  dalawlem3  39874  pmapj2N  39930  osumcllem9N  39965  pexmidlem6N  39976  4atexlemc  40070  cdleme1  40228  cdleme42a  40472  cdlemg13a  40652  cdlemh2  40817  cdlemk1  40832  tendocnv  41022  dihmeetlem12N  41319  dihmeetlem16N  41323  dihmeetlem19N  41326  dochsatshp  41452  dochexmidlem6  41466  mapdval4N  41633  mapdpglem28  41702  mapdpglem31  41704  mapdindp4  41724  hdmap14lem1a  41867  hdmapinvlem4  41922  3rdpwhole  42287  oexpreposd  42317  remul01  42402  sn-negex12  42412  sn-subeu  42422  remulinvcom  42428  sn-0tie0  42446  cnreeu  42485  fltnlta  42658  irrapxlem5  42821  pellfund14  42893  rmxdbl  42935  jm2.22  42991  oaabsb  43290  oaun2  43377  oaun3  43378  sqrtcval  43637  0ellimcdiv  45654  fourierdlem95  46206  etransclem46  46285  sigariz  46868  ichreuopeq  47478  gricushgr  47921  altgsumbc  48344  blengt1fldiv2p1  48586  restclsseplem  48907  cofu1a  49087  cofu2a  49088  uobeqw  49212  swapf2fval  49258  swapf1val  49260  coccom  49657