Theorem 3eqtr3rd 2781

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

Syntax hints:   → wi 4   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  iunxdif3  5038  fcofo  7236  fcof1oinvd  7241  cantnfp1lem3  9592  fin1a2lem7  10319  prlem934  10947  addlid  11320  addcom  11323  addcomd  11339  negeu  11374  add20  11653  2halves  12386  bcnn  14265  bcpasc  14274  hashfun  14390  hashf1dmrn  14396  wrdeqs1cat  14673  sqreulem  15313  summolem3  15667  fsumneg  15740  geolim  15826  geolim2  15827  mertens  15842  prodmolem3  15889  fallrisefac  15981  bpoly3  16014  sincossq  16134  demoivre  16158  eirrlem  16162  oddpwp1fsum  16352  sadeq  16432  gcdid  16487  gcdmultipled  16494  nn0rppwr  16521  phiprmpw  16737  pythagtriplem12  16788  expnprm  16864  fullresc  17809  grpinvid1  18958  grpnpcan  18999  grplactcnv  19010  ghmgrp  19033  conjghm  19215  odmodnn0  19506  gex1  19557  sylow3lem3  19595  efgredeu  19718  odadd2  19815  gsumval3  19873  pgpfac1lem3a  20044  omndmul2  20099  ringnegl  20274  ringnegr  20275  ringmneg2  20277  rdivmuldivd  20384  imadrhmcl  20765  lmodfopne  20886  lmodvsneg  20892  lssvs0or  21100  lvecinv  21103  lspabs2  21110  zringunit  21456  zringcyg  21459  dvdschrmulg  21518  fermltlchr  21519  sraassab  21858  mplcoe3  22026  mplcoe5  22028  evlvar  22096  psd1  22143  mdetrlin  22577  mdetunilem6  22592  cramerimplem3  22660  cramerimp  22661  paste  23269  tuslem  24241  tususs  24244  ngpds  24579  ioo2bl  24768  ipcau2  25211  dvexp3  25955  rolle  25967  cmvth  25968  dv11cn  25978  lhop  25993  itgsubstlem  26025  itgpowd  26027  ply1divex  26112  fta1glem1  26143  fta1g  26145  dgrnznn  26222  fta1  26285  vieta1lem2  26288  aaliou2  26317  dvtaylp  26347  dvntaylp  26348  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  dvradcnv  26399  ptolemy  26473  coskpi  26500  tanregt0  26516  cxpeq  26734  isosctrlem2  26796  chordthmlem  26809  dcubic  26823  quart1lem  26832  tanatan  26896  atantan  26900  dvatan  26912  birthdaylem2  26929  rlimcxp  26951  jensenlem2  26965  logdiflbnd  26972  emcllem2  26974  lgamgulmlem2  27007  lgamcvg2  27032  basellem8  27065  bclbnd  27257  lgsqr  27328  lgseisenlem3  27354  lgseisenlem4  27355  lgsquadlem1  27357  lgsquadlem2  27358  rpvmasumlem  27464  dchrisumlem1  27466  dchrisum0flblem1  27485  dchrisum0flblem2  27486  dchrisum0re  27490  dchrisum0lem1  27493  mudivsum  27507  mulogsum  27509  vmalogdivsum2  27515  logsqvma2  27520  selberg2lem  27527  logdivbnd  27533  selbergr  27545  selberg3r  27546  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntpbnd2  27564  pw2divscan4d  28450  pw2cutp1  28467  pw2cut2  28468  z12zsodd  28488  miduniq  28767  krippenlem  28772  colperpexlem2  28813  ttgcontlem1  28967  brbtwn2  28988  colinearalglem4  28992  axsegconlem9  29008  ax5seglem1  29011  axbtwnid  29022  axeuclidlem  29045  axcontlem2  29048  axcontlem4  29050  grpoinvid1  30614  vcz  30661  hosubsub4  31904  lnop0  32052  branmfn  32191  fressupp  32776  difico  32871  wrdsplex  33011  s3f1  33022  ccatf1  33024  mgcf1o  33078  mndlrinv  33099  cycpmco2lem4  33205  tocyccntz  33220  cyc3genpm  33228  cycpmconjslem2  33231  kerunit  33400  qustrivr  33440  znfermltl  33441  linds2eq  33456  dvdsruassoi  33459  dvdsruasso  33460  qsdrnglem2  33571  zringfrac  33629  m1pmeq  33660  vr1nz  33668  mplvrpmrhm  33706  esplyfval1  33732  ply1degltdimlem  33782  fedgmullem2  33790  fldextrspunlsplem  33833  constrrtll  33891  constrrtlc1  33892  constrrtcclem  33894  constrrtcc  33895  constrrecl  33929  2sqr3minply  33940  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  carsggect  34478  carsgclctunlem2  34479  ballotlemfrceq  34689  ballotlemrinv0  34693  hashreprin  34780  hgt750lemb  34816  faclimlem1  35941  irrdifflemf  37655  poimirlem4  37959  poimirlem23  37978  mblfinlem2  37993  voliunnfl  37999  volsupnfl  38000  itg2addnclem3  38008  ftc2nc  38037  dvasin  38039  areacirclem1  38043  areacirclem4  38046  rngonegmn1l  38276  rngonegmn1r  38277  lfl0  39525  latmassOLD  39689  omlmod1i2N  39720  llnexchb2lem  40328  dalawlem3  40333  pmapj2N  40389  osumcllem9N  40424  pexmidlem6N  40435  4atexlemc  40529  cdleme1  40687  cdleme42a  40931  cdlemg13a  41111  cdlemh2  41276  cdlemk1  41291  tendocnv  41481  dihmeetlem12N  41778  dihmeetlem16N  41782  dihmeetlem19N  41785  dochsatshp  41911  dochexmidlem6  41925  mapdval4N  42092  mapdpglem28  42161  mapdpglem31  42163  mapdindp4  42183  hdmap14lem1a  42326  hdmapinvlem4  42381  3rdpwhole  42738  oexpreposd  42768  remul01  42853  sn-negex12  42863  sn-subeu  42873  remulinvcom  42879  sn-0tie0  42910  cnreeu  42949  fltnlta  43110  irrapxlem5  43272  pellfund14  43344  rmxdbl  43385  jm2.22  43441  oaabsb  43740  oaun2  43827  oaun3  43828  sqrtcval  44086  0ellimcdiv  46095  fourierdlem95  46647  etransclem46  46726  sigariz  47309  sin5tlem2  47338  sin5tlem5  47341  ichreuopeq  47945  gricushgr  48405  altgsumbc  48840  blengt1fldiv2p1  49081  restclsseplem  49402  cofu1a  49581  cofu2a  49582  uobeqw  49706  swapf2fval  49752  swapf1val  49754  coccom  50151