Theorem 3eqtr3rd 2775

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 2768	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2768	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 2121  ax-ext 2703

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

This theorem is referenced by:  iunxdif3  5043  fcofo  7222  fcof1oinvd  7227  cantnfp1lem3  9570  fin1a2lem7  10297  prlem934  10924  addlid  11296  addcom  11299  addcomd  11315  negeu  11350  add20  11629  2halves  12339  bcnn  14219  bcpasc  14228  hashfun  14344  hashf1dmrn  14350  wrdeqs1cat  14627  sqreulem  15267  summolem3  15621  fsumneg  15694  geolim  15777  geolim2  15778  mertens  15793  prodmolem3  15840  fallrisefac  15932  bpoly3  15965  sincossq  16085  demoivre  16109  eirrlem  16113  oddpwp1fsum  16303  sadeq  16383  gcdid  16438  gcdmultipled  16445  nn0rppwr  16472  phiprmpw  16687  pythagtriplem12  16738  expnprm  16814  fullresc  17758  grpinvid1  18904  grpnpcan  18945  grplactcnv  18956  ghmgrp  18979  conjghm  19162  odmodnn0  19453  gex1  19504  sylow3lem3  19542  efgredeu  19665  odadd2  19762  gsumval3  19820  pgpfac1lem3a  19991  omndmul2  20046  ringnegl  20221  ringnegr  20222  ringmneg2  20224  rdivmuldivd  20332  imadrhmcl  20713  lmodfopne  20834  lmodvsneg  20840  lssvs0or  21048  lvecinv  21051  lspabs2  21058  zringunit  21404  zringcyg  21407  dvdschrmulg  21466  fermltlchr  21467  sraassab  21806  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  28884  colinearalglem4  28888  axsegconlem9  28904  ax5seglem1  28907  axbtwnid  28918  axeuclidlem  28941  axcontlem2  28944  axcontlem4  28946  grpoinvid1  30506  vcz  30553  hosubsub4  31796  lnop0  31944  branmfn  32083  fressupp  32667  difico  32764  wrdsplex  32915  s3f1  32926  ccatf1  32928  mgcf1o  32982  mndlrinv  33003  cycpmco2lem4  33096  tocyccntz  33111  cyc3genpm  33119  cycpmconjslem2  33122  kerunit  33288  qustrivr  33328  znfermltl  33329  linds2eq  33344  dvdsruassoi  33347  dvdsruasso  33348  qsdrnglem2  33459  zringfrac  33517  m1pmeq  33545  vr1nz  33552  mplvrpmrhm  33575  ply1degltdimlem  33633  fedgmullem2  33641  fldextrspunlsplem  33684  constrrtll  33742  constrrtlc1  33743  constrrtcclem  33745  constrrtcc  33746  constrrecl  33780  2sqr3minply  33791  cos9thpiminplylem1  33793  cos9thpiminplylem2  33794  carsggect  34329  carsgclctunlem2  34330  ballotlemfrceq  34540  ballotlemrinv0  34544  hashreprin  34631  hgt750lemb  34667  faclimlem1  35785  irrdifflemf  37365  poimirlem4  37670  poimirlem23  37689  mblfinlem2  37704  voliunnfl  37710  volsupnfl  37711  itg2addnclem3  37719  ftc2nc  37748  dvasin  37750  areacirclem1  37754  areacirclem4  37757  rngonegmn1l  37987  rngonegmn1r  37988  lfl0  39110  latmassOLD  39274  omlmod1i2N  39305  llnexchb2lem  39913  dalawlem3  39918  pmapj2N  39974  osumcllem9N  40009  pexmidlem6N  40020  4atexlemc  40114  cdleme1  40272  cdleme42a  40516  cdlemg13a  40696  cdlemh2  40861  cdlemk1  40876  tendocnv  41066  dihmeetlem12N  41363  dihmeetlem16N  41367  dihmeetlem19N  41370  dochsatshp  41496  dochexmidlem6  41510  mapdval4N  41677  mapdpglem28  41746  mapdpglem31  41748  mapdindp4  41768  hdmap14lem1a  41911  hdmapinvlem4  41966  3rdpwhole  42331  oexpreposd  42361  remul01  42446  sn-negex12  42456  sn-subeu  42466  remulinvcom  42472  sn-0tie0  42490  cnreeu  42529  fltnlta  42702  irrapxlem5  42865  pellfund14  42937  rmxdbl  42978  jm2.22  43034  oaabsb  43333  oaun2  43420  oaun3  43421  sqrtcval  43680  0ellimcdiv  45693  fourierdlem95  46245  etransclem46  46324  sigariz  46907  ichreuopeq  47510  gricushgr  47954  altgsumbc  48389  blengt1fldiv2p1  48631  restclsseplem  48952  cofu1a  49132  cofu2a  49133  uobeqw  49257  swapf2fval  49303  swapf1val  49305  coccom  49702