Theorem 3eqtr3rd 2807

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

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  iunxdif3  5062  fcofo  7288  fcof1oinvd  7293  cantnfp1lem3  9650  fin1a2lem7  10391  prlem934  11019  addlid  11394  addcom  11397  addcomd  11413  negeu  11448  add20  11727  2halves  12463  bcnn  14350  bcpasc  14359  hashfun  14476  hashf1dmrn  14482  wrdeqs1cat  14759  sqreulem  15413  summolem3  15767  fsumneg  15840  geolim  15926  geolim2  15927  mertens  15942  prodmolem3  15989  fallrisefac  16081  bpoly3  16113  sincossq  16233  demoivre  16257  eirrlem  16261  oddpwp1fsum  16451  sadeq  16531  gcdid  16586  gcdmultipled  16593  nn0rppwr  16620  phiprmpw  16836  pythagtriplem12  16887  expnprm  16963  fullresc  17909  grpinvid1  19059  grpnpcan  19099  grplactcnv  19110  ghmgrp  19133  qustrivr  19254  conjghm  19320  odmodnn0  19611  gex1  19662  sylow3lem3  19700  efgredeu  19823  odadd2  19920  gsumval3  19978  pgpfac1lem3a  20149  omndmul2  20204  ringnegl  20386  ringnegr  20387  ringmneg2  20389  rdivmuldivd  20496  imadrhmcl  20881  lmodfopne  21002  lmodvsneg  21008  lssvs0or  21215  lvecinv  21218  lspabs2  21225  zringunit  21597  zringcyg  21600  dvdschrmulg  21659  fermltlchr  21660  sraassab  21999  mplcoe3  22170  mplcoe5  22172  evlvar  22240  psd1  22311  mdetrlin  22740  mdetunilem6  22755  cramerimplem3  22823  cramerimp  22824  paste  23432  tuslem  24404  tususs  24407  ngpds  24742  ioo2bl  24931  ipcau2  25374  dvexp3  26118  rolle  26130  cmvth  26131  dv11cn  26141  lhop  26156  itgsubstlem  26188  itgpowd  26190  ply1divex  26275  fta1glem1  26306  fta1g  26308  dgrnznn  26385  fta1  26450  vieta1lem2  26453  aaliou2  26482  dvtaylp  26511  dvntaylp  26512  taylthlem1  26514  taylthlem2  26515  dvradcnv  26562  ptolemy  26639  coskpi  26666  tanregt0  26682  cxpeq  26900  isosctrlem2  26962  chordthmlem  26975  dcubic  26989  quart1lem  26998  tanatan  27062  atantan  27066  dvatan  27078  birthdaylem2  27095  rlimcxp  27116  jensenlem2  27130  logdiflbnd  27137  emcllem2  27139  lgamgulmlem2  27172  lgamcvg2  27197  basellem8  27230  bclbnd  27422  lgsqr  27493  lgseisenlem3  27519  lgseisenlem4  27520  lgsquadlem1  27522  lgsquadlem2  27523  rpvmasumlem  27629  dchrisumlem1  27631  dchrisum0flblem1  27650  dchrisum0flblem2  27651  dchrisum0re  27655  dchrisum0lem1  27658  mudivsum  27672  mulogsum  27674  vmalogdivsum2  27680  logsqvma2  27685  selberg2lem  27692  logdivbnd  27698  selbergr  27710  selberg3r  27711  pntrlog2bndlem4  27722  pntrlog2bndlem5  27723  pntpbnd2  27729  pw2divscan4d  28615  pw2cutp1  28632  pw2cut2  28633  z12zsodd  28653  miduniq  28940  krippenlem  28945  colperpexlem2  28990  plngrotlem1  29047  ttgcontlem1  29212  brbtwn2  29233  colinearalglem4  29237  axsegconlem9  29253  ax5seglem1  29256  axbtwnid  29267  axeuclidlem  29290  axcontlem2  29293  axcontlem4  29295  grpoinvid1  30858  vcz  30905  hosubsub4  32148  lnop0  32296  branmfn  32435  fressupp  33011  difico  33106  wrdsplex  33234  s3f1  33245  ccatf1  33247  mgcf1o  33301  mndlrinv  33322  cycpmco2lem4  33427  tocyccntz  33442  cyc3genpm  33450  cycpmconjslem2  33453  rlocisunit  33574  kerunit  33623  znfermltl  33659  linds2eq  33672  dvdsruassoi  33675  dvdsruasso  33676  qsdrnglem2  33756  zringfrac  33822  m1pmeq  33853  vr1nz  33861  mplvrpmrhm  33915  esplyfval1  33941  ply1degltdimlem  33990  fedgmullem2  33998  fldextrspunlsplem  34041  constrrtll  34099  constrrtlc1  34100  constrrtcclem  34102  constrrtcc  34103  constrrecl  34137  2sqr3minply  34148  cos9thpiminplylem1  34150  cos9thpiminplylem2  34151  carsggect  34686  carsgclctunlem2  34687  ballotlemfrceq  34897  ballotlemrinv0  34901  hashreprin  34985  hgt750lemb  35021  faclimlem1  36213  irrdifflemf  37947  poimirlem4  38253  poimirlem23  38272  mblfinlem2  38287  voliunnfl  38293  volsupnfl  38294  itg2addnclem3  38302  ftc2nc  38331  dvasin  38333  areacirclem1  38337  areacirclem4  38340  rngonegmn1l  38570  rngonegmn1r  38571  lfl0  39817  latmassOLD  39981  omlmod1i2N  40012  llnexchb2lem  40620  dalawlem3  40625  pmapj2N  40681  osumcllem9N  40716  pexmidlem6N  40727  4atexlemc  40821  cdleme1  40979  cdleme42a  41223  cdlemg13a  41403  cdlemh2  41568  cdlemk1  41583  tendocnv  41773  dihmeetlem12N  42070  dihmeetlem16N  42074  dihmeetlem19N  42077  dochsatshp  42203  dochexmidlem6  42217  mapdval4N  42384  mapdpglem28  42453  mapdpglem31  42455  mapdindp4  42475  hdmap14lem1a  42618  hdmapinvlem4  42673  3rdpwhole  43031  oexpreposd  43061  remul01  43146  sn-negex12  43156  sn-subeu  43166  remulinvcom  43172  sn-0tie0  43203  cnreeu  43242  fltnlta  43375  irrapxlem5  43533  pellfund14  43605  rmxdbl  43646  jm2.22  43702  oaabsb  44001  oaun2  44088  oaun3  44089  sqrtcval  44347  0ellimcdiv  46343  fourierdlem95  46895  etransclem46  46974  sigariz  47557  sin5tlem2  47588  sin5tlem5  47591  cos5t  47593  ichreuopeq  48199  gricushgr  48659  altgsumbc  49109  blengt1fldiv2p1  49350  restclsseplem  49670  cofu1a  49849  cofu2a  49850  uobeqw  49974  swapf2fval  50020  swapf1val  50022  coccom  50419