Theorem 3eqtr3rd 2777

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  iunxdif3  5045  fcofo  7228  fcof1oinvd  7233  cantnfp1lem3  9577  fin1a2lem7  10304  prlem934  10931  addlid  11303  addcom  11306  addcomd  11322  negeu  11357  add20  11636  2halves  12346  bcnn  14221  bcpasc  14230  hashfun  14346  hashf1dmrn  14352  wrdeqs1cat  14629  sqreulem  15269  summolem3  15623  fsumneg  15696  geolim  15779  geolim2  15780  mertens  15795  prodmolem3  15842  fallrisefac  15934  bpoly3  15967  sincossq  16087  demoivre  16111  eirrlem  16115  oddpwp1fsum  16305  sadeq  16385  gcdid  16440  gcdmultipled  16447  nn0rppwr  16474  phiprmpw  16689  pythagtriplem12  16740  expnprm  16816  fullresc  17760  grpinvid1  18906  grpnpcan  18947  grplactcnv  18958  ghmgrp  18981  conjghm  19163  odmodnn0  19454  gex1  19505  sylow3lem3  19543  efgredeu  19666  odadd2  19763  gsumval3  19821  pgpfac1lem3a  19992  omndmul2  20047  ringnegl  20222  ringnegr  20223  ringmneg2  20225  rdivmuldivd  20333  imadrhmcl  20714  lmodfopne  20835  lmodvsneg  20841  lssvs0or  21049  lvecinv  21052  lspabs2  21059  zringunit  21405  zringcyg  21408  dvdschrmulg  21467  fermltlchr  21468  sraassab  21807  mplcoe3  21974  mplcoe5  21976  evlvar  22036  psd1  22083  mdetrlin  22518  mdetunilem6  22533  cramerimplem3  22601  cramerimp  22602  paste  23210  tuslem  24182  tususs  24185  ngpds  24520  ioo2bl  24709  ipcau2  25162  dvexp3  25910  rolle  25922  cmvth  25923  cmvthOLD  25924  dv11cn  25934  lhop  25949  itgsubstlem  25983  itgpowd  25985  ply1divex  26070  fta1glem1  26101  fta1g  26103  dgrnznn  26180  fta1  26244  vieta1lem2  26247  aaliou2  26276  dvtaylp  26306  dvntaylp  26307  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  dvradcnv  26358  ptolemy  26433  coskpi  26460  tanregt0  26476  cxpeq  26695  isosctrlem2  26757  chordthmlem  26770  dcubic  26784  quart1lem  26793  tanatan  26857  atantan  26861  dvatan  26873  birthdaylem2  26890  rlimcxp  26912  jensenlem2  26926  logdiflbnd  26933  emcllem2  26935  lgamgulmlem2  26968  lgamcvg2  26993  basellem8  27026  bclbnd  27219  lgsqr  27290  lgseisenlem3  27316  lgseisenlem4  27317  lgsquadlem1  27319  lgsquadlem2  27320  rpvmasumlem  27426  dchrisumlem1  27428  dchrisum0flblem1  27447  dchrisum0flblem2  27448  dchrisum0re  27452  dchrisum0lem1  27455  mudivsum  27469  mulogsum  27471  vmalogdivsum2  27477  logsqvma2  27482  selberg2lem  27489  logdivbnd  27495  selbergr  27507  selberg3r  27508  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntpbnd2  27526  pw2divscan4d  28368  pw2cutp1  28382  pw2cut2  28383  zs12zodd  28393  miduniq  28664  krippenlem  28669  colperpexlem2  28710  ttgcontlem1  28864  brbtwn2  28885  colinearalglem4  28889  axsegconlem9  28905  ax5seglem1  28908  axbtwnid  28919  axeuclidlem  28942  axcontlem2  28945  axcontlem4  28947  grpoinvid1  30510  vcz  30557  hosubsub4  31800  lnop0  31948  branmfn  32087  fressupp  32673  difico  32770  wrdsplex  32924  s3f1  32935  ccatf1  32937  mgcf1o  32991  mndlrinv  33012  cycpmco2lem4  33105  tocyccntz  33120  cyc3genpm  33128  cycpmconjslem2  33131  kerunit  33297  qustrivr  33337  znfermltl  33338  linds2eq  33353  dvdsruassoi  33356  dvdsruasso  33357  qsdrnglem2  33468  zringfrac  33526  m1pmeq  33554  vr1nz  33561  mplvrpmrhm  33595  ply1degltdimlem  33656  fedgmullem2  33664  fldextrspunlsplem  33707  constrrtll  33765  constrrtlc1  33766  constrrtcclem  33768  constrrtcc  33769  constrrecl  33803  2sqr3minply  33814  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  carsggect  34352  carsgclctunlem2  34353  ballotlemfrceq  34563  ballotlemrinv0  34567  hashreprin  34654  hgt750lemb  34690  faclimlem1  35808  irrdifflemf  37390  poimirlem4  37685  poimirlem23  37704  mblfinlem2  37719  voliunnfl  37725  volsupnfl  37726  itg2addnclem3  37734  ftc2nc  37763  dvasin  37765  areacirclem1  37769  areacirclem4  37772  rngonegmn1l  38002  rngonegmn1r  38003  lfl0  39185  latmassOLD  39349  omlmod1i2N  39380  llnexchb2lem  39988  dalawlem3  39993  pmapj2N  40049  osumcllem9N  40084  pexmidlem6N  40095  4atexlemc  40189  cdleme1  40347  cdleme42a  40591  cdlemg13a  40771  cdlemh2  40936  cdlemk1  40951  tendocnv  41141  dihmeetlem12N  41438  dihmeetlem16N  41442  dihmeetlem19N  41445  dochsatshp  41571  dochexmidlem6  41585  mapdval4N  41752  mapdpglem28  41821  mapdpglem31  41823  mapdindp4  41843  hdmap14lem1a  41986  hdmapinvlem4  42041  3rdpwhole  42411  oexpreposd  42441  remul01  42526  sn-negex12  42536  sn-subeu  42546  remulinvcom  42552  sn-0tie0  42570  cnreeu  42609  fltnlta  42782  irrapxlem5  42944  pellfund14  43016  rmxdbl  43057  jm2.22  43113  oaabsb  43412  oaun2  43499  oaun3  43500  sqrtcval  43759  0ellimcdiv  45772  fourierdlem95  46324  etransclem46  46403  sigariz  46986  ichreuopeq  47598  gricushgr  48042  altgsumbc  48477  blengt1fldiv2p1  48719  restclsseplem  49040  cofu1a  49220  cofu2a  49221  uobeqw  49345  swapf2fval  49391  swapf1val  49393  coccom  49790