Theorem 3eqtr3rd 2773

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

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

This theorem is referenced by:  iunxdif3  5059  fcofo  7263  fcof1oinvd  7268  cantnfp1lem3  9633  fin1a2lem7  10359  prlem934  10986  addlid  11357  addcom  11360  addcomd  11376  negeu  11411  add20  11690  2halves  12400  bcnn  14277  bcpasc  14286  hashfun  14402  hashf1dmrn  14408  wrdeqs1cat  14685  sqreulem  15326  summolem3  15680  fsumneg  15753  geolim  15836  geolim2  15837  mertens  15852  prodmolem3  15899  fallrisefac  15991  bpoly3  16024  sincossq  16144  demoivre  16168  eirrlem  16172  oddpwp1fsum  16362  sadeq  16442  gcdid  16497  gcdmultipled  16504  nn0rppwr  16531  phiprmpw  16746  pythagtriplem12  16797  expnprm  16873  fullresc  17813  grpinvid1  18923  grpnpcan  18964  grplactcnv  18975  ghmgrp  18998  conjghm  19181  odmodnn0  19470  gex1  19521  sylow3lem3  19559  efgredeu  19682  odadd2  19779  gsumval3  19837  pgpfac1lem3a  20008  ringnegl  20211  ringnegr  20212  ringmneg2  20214  rdivmuldivd  20322  imadrhmcl  20706  lmodfopne  20806  lmodvsneg  20812  lssvs0or  21020  lvecinv  21023  lspabs2  21030  zringunit  21376  zringcyg  21379  dvdschrmulg  21438  fermltlchr  21439  sraassab  21777  mplcoe3  21945  mplcoe5  21947  evlvar  22007  psd1  22054  mdetrlin  22489  mdetunilem6  22504  cramerimplem3  22572  cramerimp  22573  paste  23181  tuslem  24154  tususs  24157  ngpds  24492  ioo2bl  24681  ipcau2  25134  dvexp3  25882  rolle  25894  cmvth  25895  cmvthOLD  25896  dv11cn  25906  lhop  25921  itgsubstlem  25955  itgpowd  25957  ply1divex  26042  fta1glem1  26073  fta1g  26075  dgrnznn  26152  fta1  26216  vieta1lem2  26219  aaliou2  26248  dvtaylp  26278  dvntaylp  26279  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  dvradcnv  26330  ptolemy  26405  coskpi  26432  tanregt0  26448  cxpeq  26667  isosctrlem2  26729  chordthmlem  26742  dcubic  26756  quart1lem  26765  tanatan  26829  atantan  26833  dvatan  26845  birthdaylem2  26862  rlimcxp  26884  jensenlem2  26898  logdiflbnd  26905  emcllem2  26907  lgamgulmlem2  26940  lgamcvg2  26965  basellem8  26998  bclbnd  27191  lgsqr  27262  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem2  27292  rpvmasumlem  27398  dchrisumlem1  27400  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0re  27424  dchrisum0lem1  27427  mudivsum  27441  mulogsum  27443  vmalogdivsum2  27449  logsqvma2  27454  selberg2lem  27461  logdivbnd  27467  selbergr  27479  selberg3r  27480  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntpbnd2  27498  pw2cutp1  28336  miduniq  28612  krippenlem  28617  colperpexlem2  28658  ttgcontlem1  28812  brbtwn2  28832  colinearalglem4  28836  axsegconlem9  28852  ax5seglem1  28855  axbtwnid  28866  axeuclidlem  28889  axcontlem2  28892  axcontlem4  28894  grpoinvid1  30457  vcz  30504  hosubsub4  31747  lnop0  31895  branmfn  32034  fressupp  32611  difico  32706  wrdsplex  32857  s3f1  32868  ccatf1  32870  mgcf1o  32929  mndlrinv  32965  omndmul2  33026  cycpmco2lem4  33086  tocyccntz  33101  cyc3genpm  33109  cycpmconjslem2  33112  kerunit  33297  qustrivr  33336  znfermltl  33337  linds2eq  33352  dvdsruassoi  33355  dvdsruasso  33356  qsdrnglem2  33467  zringfrac  33525  m1pmeq  33552  vr1nz  33559  ply1degltdimlem  33618  fedgmullem2  33626  fldextrspunlsplem  33668  constrrtll  33721  constrrtlc1  33722  constrrtcclem  33724  constrrtcc  33725  constrrecl  33759  2sqr3minply  33770  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  carsggect  34309  carsgclctunlem2  34310  ballotlemfrceq  34520  ballotlemrinv0  34524  hashreprin  34611  hgt750lemb  34647  faclimlem1  35730  irrdifflemf  37313  poimirlem4  37618  poimirlem23  37637  mblfinlem2  37652  voliunnfl  37658  volsupnfl  37659  itg2addnclem3  37667  ftc2nc  37696  dvasin  37698  areacirclem1  37702  areacirclem4  37705  rngonegmn1l  37935  rngonegmn1r  37936  lfl0  39058  latmassOLD  39222  omlmod1i2N  39253  llnexchb2lem  39862  dalawlem3  39867  pmapj2N  39923  osumcllem9N  39958  pexmidlem6N  39969  4atexlemc  40063  cdleme1  40221  cdleme42a  40465  cdlemg13a  40645  cdlemh2  40810  cdlemk1  40825  tendocnv  41015  dihmeetlem12N  41312  dihmeetlem16N  41316  dihmeetlem19N  41319  dochsatshp  41445  dochexmidlem6  41459  mapdval4N  41626  mapdpglem28  41695  mapdpglem31  41697  mapdindp4  41717  hdmap14lem1a  41860  hdmapinvlem4  41915  3rdpwhole  42280  oexpreposd  42310  remul01  42395  sn-negex12  42405  sn-subeu  42415  remulinvcom  42421  sn-0tie0  42439  cnreeu  42478  fltnlta  42651  irrapxlem5  42814  pellfund14  42886  rmxdbl  42928  jm2.22  42984  oaabsb  43283  oaun2  43370  oaun3  43371  sqrtcval  43630  0ellimcdiv  45647  fourierdlem95  46199  etransclem46  46278  sigariz  46861  ichreuopeq  47474  gricushgr  47917  altgsumbc  48340  blengt1fldiv2p1  48582  restclsseplem  48903  cofu1a  49083  cofu2a  49084  uobeqw  49208  swapf2fval  49254  swapf1val  49256  coccom  49653