Theorem 3eqtr3rd 2780

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

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

This theorem is referenced by:  iunxdif3  5050  fcofo  7234  fcof1oinvd  7239  cantnfp1lem3  9589  fin1a2lem7  10316  prlem934  10944  addlid  11316  addcom  11319  addcomd  11335  negeu  11370  add20  11649  2halves  12359  bcnn  14235  bcpasc  14244  hashfun  14360  hashf1dmrn  14366  wrdeqs1cat  14643  sqreulem  15283  summolem3  15637  fsumneg  15710  geolim  15793  geolim2  15794  mertens  15809  prodmolem3  15856  fallrisefac  15948  bpoly3  15981  sincossq  16101  demoivre  16125  eirrlem  16129  oddpwp1fsum  16319  sadeq  16399  gcdid  16454  gcdmultipled  16461  nn0rppwr  16488  phiprmpw  16703  pythagtriplem12  16754  expnprm  16830  fullresc  17775  grpinvid1  18921  grpnpcan  18962  grplactcnv  18973  ghmgrp  18996  conjghm  19178  odmodnn0  19469  gex1  19520  sylow3lem3  19558  efgredeu  19681  odadd2  19778  gsumval3  19836  pgpfac1lem3a  20007  omndmul2  20062  ringnegl  20237  ringnegr  20238  ringmneg2  20240  rdivmuldivd  20349  imadrhmcl  20730  lmodfopne  20851  lmodvsneg  20857  lssvs0or  21065  lvecinv  21068  lspabs2  21075  zringunit  21421  zringcyg  21424  dvdschrmulg  21483  fermltlchr  21484  sraassab  21823  mplcoe3  21993  mplcoe5  21995  evlvar  22063  psd1  22110  mdetrlin  22546  mdetunilem6  22561  cramerimplem3  22629  cramerimp  22630  paste  23238  tuslem  24210  tususs  24213  ngpds  24548  ioo2bl  24737  ipcau2  25190  dvexp3  25938  rolle  25950  cmvth  25951  cmvthOLD  25952  dv11cn  25962  lhop  25977  itgsubstlem  26011  itgpowd  26013  ply1divex  26098  fta1glem1  26129  fta1g  26131  dgrnznn  26208  fta1  26272  vieta1lem2  26275  aaliou2  26304  dvtaylp  26334  dvntaylp  26335  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  dvradcnv  26386  ptolemy  26461  coskpi  26488  tanregt0  26504  cxpeq  26723  isosctrlem2  26785  chordthmlem  26798  dcubic  26812  quart1lem  26821  tanatan  26885  atantan  26889  dvatan  26901  birthdaylem2  26918  rlimcxp  26940  jensenlem2  26954  logdiflbnd  26961  emcllem2  26963  lgamgulmlem2  26996  lgamcvg2  27021  basellem8  27054  bclbnd  27247  lgsqr  27318  lgseisenlem3  27344  lgseisenlem4  27345  lgsquadlem1  27347  lgsquadlem2  27348  rpvmasumlem  27454  dchrisumlem1  27456  dchrisum0flblem1  27475  dchrisum0flblem2  27476  dchrisum0re  27480  dchrisum0lem1  27483  mudivsum  27497  mulogsum  27499  vmalogdivsum2  27505  logsqvma2  27510  selberg2lem  27517  logdivbnd  27523  selbergr  27535  selberg3r  27536  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntpbnd2  27554  pw2divscan4d  28440  pw2cutp1  28457  pw2cut2  28458  z12zsodd  28478  miduniq  28757  krippenlem  28762  colperpexlem2  28803  ttgcontlem1  28957  brbtwn2  28978  colinearalglem4  28982  axsegconlem9  28998  ax5seglem1  29001  axbtwnid  29012  axeuclidlem  29035  axcontlem2  29038  axcontlem4  29040  grpoinvid1  30603  vcz  30650  hosubsub4  31893  lnop0  32041  branmfn  32180  fressupp  32767  difico  32863  wrdsplex  33018  s3f1  33029  ccatf1  33031  mgcf1o  33085  mndlrinv  33106  cycpmco2lem4  33211  tocyccntz  33226  cyc3genpm  33234  cycpmconjslem2  33237  kerunit  33406  qustrivr  33446  znfermltl  33447  linds2eq  33462  dvdsruassoi  33465  dvdsruasso  33466  qsdrnglem2  33577  zringfrac  33635  m1pmeq  33666  vr1nz  33674  mplvrpmrhm  33712  ply1degltdimlem  33779  fedgmullem2  33787  fldextrspunlsplem  33830  constrrtll  33888  constrrtlc1  33889  constrrtcclem  33891  constrrtcc  33892  constrrecl  33926  2sqr3minply  33937  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  carsggect  34475  carsgclctunlem2  34476  ballotlemfrceq  34686  ballotlemrinv0  34690  hashreprin  34777  hgt750lemb  34813  faclimlem1  35937  irrdifflemf  37526  poimirlem4  37821  poimirlem23  37840  mblfinlem2  37855  voliunnfl  37861  volsupnfl  37862  itg2addnclem3  37870  ftc2nc  37899  dvasin  37901  areacirclem1  37905  areacirclem4  37908  rngonegmn1l  38138  rngonegmn1r  38139  lfl0  39321  latmassOLD  39485  omlmod1i2N  39516  llnexchb2lem  40124  dalawlem3  40129  pmapj2N  40185  osumcllem9N  40220  pexmidlem6N  40231  4atexlemc  40325  cdleme1  40483  cdleme42a  40727  cdlemg13a  40907  cdlemh2  41072  cdlemk1  41087  tendocnv  41277  dihmeetlem12N  41574  dihmeetlem16N  41578  dihmeetlem19N  41581  dochsatshp  41707  dochexmidlem6  41721  mapdval4N  41888  mapdpglem28  41957  mapdpglem31  41959  mapdindp4  41979  hdmap14lem1a  42122  hdmapinvlem4  42177  3rdpwhole  42543  oexpreposd  42573  remul01  42658  sn-negex12  42668  sn-subeu  42678  remulinvcom  42684  sn-0tie0  42702  cnreeu  42741  fltnlta  42902  irrapxlem5  43064  pellfund14  43136  rmxdbl  43177  jm2.22  43233  oaabsb  43532  oaun2  43619  oaun3  43620  sqrtcval  43878  0ellimcdiv  45889  fourierdlem95  46441  etransclem46  46520  sigariz  47103  ichreuopeq  47715  gricushgr  48159  altgsumbc  48594  blengt1fldiv2p1  48835  restclsseplem  49156  cofu1a  49335  cofu2a  49336  uobeqw  49460  swapf2fval  49506  swapf1val  49508  coccom  49905