Theorem 3eqtr4rd 2788

Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)

Hypotheses

Ref	Expression
3eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr4rd

Step	Hyp	Ref	Expression
1		3eqtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
2		3eqtr4d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtr4d 2780	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2780	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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  csbun  4441  csbdif  4524  csbcnvgALT  5895  csbres  6000  fimacnvinrn2  7092  f1ossf1o  7148  suppvalbr  8189  odi  8617  phplem2  9245  phplem4OLD  9257  cantnfp1lem3  9720  cantnfp1  9721  cardidm  9999  ackbij2lem2  10279  ackbij2lem3  10280  divneg  11959  xadddilem  13336  xadddi2  13339  dfceil2  13879  modlt  13920  modmulnn  13929  seqcaopr3  14078  bcval5  14357  hashgadd  14416  hashun3  14423  hashmap  14474  seqcoll  14503  revccat  14804  cshwmodn  14833  2cshwcom  14854  cshimadifsn0  14869  revco  14873  cshco  14875  ofccat  15008  relexpsucl  15070  dfrtrclrec2  15097  cjreb  15162  recj  15163  imcj  15171  imval2  15190  sqrtmul  15298  absmax  15368  amgm2  15408  summolem2a  15751  fsumf1o  15759  sumsnf  15779  sumsplit  15804  fsummulc2  15820  binom  15866  bcxmas  15871  incexclem  15872  incexc  15873  expcnv  15900  pwdif  15904  cvgrat  15919  prodmolem3  15969  prodmolem2a  15970  fprodf1o  15982  prodsn  15998  prodsnf  16000  fprodabs  16010  binomfallfac  16077  fallfacval4  16079  bcfallfac  16080  ege2le3  16126  efaddlem  16129  eftlub  16145  tanval3  16170  tanneg  16184  cosmul  16209  cos01bnd  16222  demoivreALT  16237  flodddiv4  16452  absmulgcd  16586  nn0expgcd  16601  lcmfunsnlem2  16677  eulerthlem2  16819  phisum  16828  pythagtriplem14  16866  pythagtriplem19  16871  pcmul  16889  pcfac  16937  prmreclem6  16959  4sqlem12  16994  vdwlem6  17024  oppccatid  17762  curf2ndf  18292  oppcyon  18314  joincomALT  18446  meetcomALT  18448  pwsco1mhm  18845  sgrp2nmndlem4  18941  qusgrp2  19076  mulgnngsum  19097  mulgnn0p1  19103  mulgneg  19110  mulgnn0dir  19122  qusghm  19273  gaid  19317  symgval  19388  pmtrdifellem3  19496  psgnunilem2  19513  odmulg  19574  sylow1lem2  19617  sylow2a  19637  sylow3lem1  19645  efgredleme  19761  efgcpbllemb  19773  gsumzaddlem  19939  gsumconst  19952  gsumzmhm  19955  ablsimpgfindlem1  20127  srgpcomp  20215  srgbinom  20228  rdivmuldivd  20413  c0mgm  20459  c0mhm  20460  zrrnghm  20536  imadrhmcl  20798  lmodvsmmulgdi  20895  lmodsubdi  20917  rmodislmodlem  20927  0lmhm  21039  lspsneq  21124  qusrhm  21286  quscrng  21293  zringlpirlem3  21475  mulgrhm  21488  phssip  21676  frlmip  21798  frlmphl  21801  asclmulg  21922  resspsrmul  21996  evlsscasrng  22121  psdadd  22167  psdvsca  22168  psdmul  22170  psdpw  22174  psropprmul  22239  evls1scasrng  22343  mat1ghm  22489  mat1mhm  22490  1marepvmarrepid  22581  mdetrlin  22608  mdetrsca2  22610  mdetunilem7  22624  mdetunilem9  22626  mndifsplit  22642  maducoeval2  22646  smadiadetglem2  22678  decpmatmul  22778  pm2mpghm  22822  pm2mpmhmlem2  22825  cpmidgsum2  22885  ptbasfi  23589  ptuni  23602  alexsubALTlem3  24057  subgtgp  24113  tsmsxplem1  24161  xmsusp  24582  restmetu  24583  nminv  24634  nrginvrcnlem  24712  copco  25051  pcoass  25057  pi1bas  25071  pi1xfrf  25086  pi1xfr  25088  isclmp  25130  cph2subdi  25244  cphassr  25246  tcphcphlem1  25269  cphipval  25277  rrxip  25424  rrxnm  25425  pjthlem1  25471  ovolunlem1a  25531  ovolfs2  25606  uniiccdif  25613  ismbf  25663  itgaddlem2  25859  ditgswap  25894  ply1divex  26176  plyeq0lem  26249  plymullem1  26253  dgrcolem1  26313  dgrcolem2  26314  vieta1lem2  26353  elqaalem2  26362  elqaalem3  26363  aaliou3lem7  26391  ulmshft  26433  mulcxplem  26726  cxpmul2  26731  root1eq1  26798  cxpeq  26800  logbchbase  26814  cosangneg2d  26850  isosctrlem2  26862  angpieqvdlem  26871  chordthmlem3  26877  chordthmlem4  26878  chordthmlem5  26879  quad2  26882  dcubic2  26887  cubic2  26891  quart1  26899  scvxcvx  27029  igamlgam  27093  lgam1  27107  basellem9  27132  ppifl  27203  mumul  27224  sgmmul  27245  chtublem  27255  chpub  27264  logfacrlim  27268  dchrsum2  27312  sumdchr2  27314  bposlem9  27336  lgsdir2  27374  lgsdir  27376  lgsdi  27378  lgsdirnn0  27388  lgsdinn0  27389  lgsquad3  27431  2sqblem  27475  chpo1ub  27524  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasum2if  27541  dchrisum0fmul  27550  rpvmasum2  27556  mulog2sumlem1  27578  vmalogdivsum2  27582  log2sumbnd  27588  selberg3lem1  27601  selberg4lem1  27604  pntrsumo1  27609  selbergr  27612  pntpbnd1  27630  pntlemk  27650  mulsunif2lem  28195  divsasswd  28228  absmuls  28268  zscut  28393  expsp1  28412  tgbtwnconn1lem3  28582  mideulem2  28742  axlowdimlem16  28972  axcontlem8  28986  vtxval  29017  iedgval  29018  edgval  29066  vtxdgop  29488  finsumvtxdg2size  29568  lp1cycl  30171  ex-ind-dvds  30480  vsfval  30652  lnocoi  30776  nmblolbii  30818  ipasslem5  30854  hvsubid  31045  sshjval3  31373  pjhthlem1  31410  adjval  31909  unopf1o  31935  kbpj  31975  lnopmi  32019  nmcoplbi  32047  cnlnadjlem2  32087  adjadd  32112  branmfn  32124  pjtoi  32198  ofoprabco  32674  supppreima  32700  hashxpe  32811  ccatws1f1o  32936  splfv3  32943  xrsmulgzz  33011  mndractfo  33034  mndlactf1o  33035  mndractf1o  33036  gsumfs2d  33058  psgnfzto1stlem  33120  cycpmco2lem5  33150  cycpmco2lem6  33151  cyc3co2  33160  tocyccntz  33164  cyc3genpmlem  33171  cyc3conja  33177  archiabllem1a  33198  gsumvsca1  33232  gsumvsca2  33233  elrgspnlem2  33247  elrgspnsubrunlem1  33251  rloccring  33274  imaslmod  33381  elrspunidl  33456  mxidlirredi  33499  opprabs  33510  qsdrngi  33523  1arithidomlem1  33563  1arithidomlem2  33564  zringfrac  33582  ply1degltdimlem  33673  fedgmullem1  33680  fldextrspunlsplem  33723  algextdeglem4  33761  constrconj  33786  submat1n  33804  submatres  33805  madjusmdetlem3  33828  xrge0iifhom  33936  qqhval2lem  33982  qqhrhm  33990  qqhucn  33993  esumsnf  34065  measvunilem0  34214  carsgclctunlem1  34319  ballotlemfp1  34494  ballotlemsf1o  34516  signstfveq0  34592  breprexplemc  34647  breprexp  34648  breprexpnat  34649  circlemeth  34655  logdivsqrle  34665  hgt750lema  34672  revwlk  35130  cvmlift3lem2  35325  cvmlift3lem4  35327  cvmlift3lem5  35328  cvmlift3lem6  35329  cvmlift3lem9  35332  elmrsubrn  35525  bccolsum  35739  bj-bary1lem  37311  finixpnum  37612  poimirlem4  37631  poimirlem16  37643  poimirlem19  37646  poimirlem25  37652  mblfinlem3  37666  dvtan  37677  itg2addnc  37681  itgaddnclem2  37686  ftc1anclem6  37705  areacirclem5  37719  areacirc  37720  upixp  37736  prdsbnd2  37802  ismrer1  37845  rngoneglmul  37950  rngoisocnv  37988  islshpsm  38981  lshpnel2N  38986  lfl0f  39070  ldualvsdi1  39144  ldualgrplem  39146  cmtcomlemN  39249  cvlsupr8  39350  pmodl42N  39853  pmapjat1  39855  llnmod2i2  39865  dalawlem2  39874  pmapj2N  39931  idltrn  40152  cdlemc6  40198  cdleme20d  40314  cdleme22e  40346  cdleme22eALTN  40347  cdleme35b  40452  cdleme48fvg  40502  cdlemg4d  40615  cdlemg8a  40629  cdlemg42  40731  cdlemg47a  40736  tendodi1  40786  tendodi2  40787  cdlemk4  40836  cdlemk21N  40875  cdlemk22  40895  cdlemky  40928  cdlemk53b  40958  cdlemk53  40959  cdlemkyyN  40964  erngdvlem3-rN  41000  tendocnv  41023  dia1dim2  41064  dicvaddcl  41192  dihglblem3N  41297  dihmeetlem4preN  41308  dihmeet2  41348  lcfl7lem  41501  baerlem3lem1  41709  baerlem5alem1  41710  mapdh6bN  41739  mapdh6cN  41740  mapdh6dN  41741  hdmap1l6b  41813  hdmap1l6c  41814  hdmap1l6d  41815  hdmap14lem13  41882  ofun  42277  grpcominv1  42518  evlselv  42597  flt4lem7  42669  3cubeslem2  42696  3cubeslem3r  42698  3cubeslem4  42700  pellexlem2  42841  rmxyneg  42932  oddcomabszz  42956  acongeq  42995  hausgraph  43217  onsupnmax  43240  tfsconcatrev  43361  naddass1  43406  fsovrfovd  44022  inductionexd  44168  expgrowth  44354  binomcxplemwb  44367  binomcxplemnn0  44368  binomcxplemnotnn0  44375  sumsnd  45031  restuni4  45126  fmuldfeqlem1  45597  cncfmptss  45602  climexp  45620  dvresntr  45933  stoweidlem17  46032  wallispi  46085  dirkertrigeq  46116  dirkercncflem2  46119  fourierdlem30  46152  fourierdlem41  46163  fourierdlem81  46202  fourierdlem103  46224  sge0xp  46444  sge0isummpt2  46447  isomennd  46546  vonioolem1  46695  sigarperm  46875  fcores  47079  imasetpreimafvbijlemfo  47392  fundcmpsurbijinjpreimafv  47394  fundcmpsurinjimaid  47398  prprspr2  47505  opoeALTV  47670  uhgrimisgrgric  47899  isubgr3stgrlem2  47934  cznrng  48177  rngchomrnghmresALTV  48195  fdmdifeqresdif  48258  lincsum  48346  lincscm  48347  lmod1lem4  48407  blennngt2o2  48513  blennn0e2  48515  tposideq  48788  topdlat  48893  swapfid  48985  swapfcoa  48987  oppgoppchom  49187  oppgoppcco  49188  oppgoppcid  49189  reccot  49277  rectan  49278  cotsqcscsq  49281  amgmlemALT  49322