Theorem 3eqtr4rd 2869

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 2861	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2861	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1537

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 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  csbun  4392  csbcnvgALT  5757  csbres  5858  fimacnvinrn2  6843  f1ossf1o  6892  odi  8207  phplem4  8701  cantnfp1lem3  9145  cantnfp1  9146  cardidm  9390  ackbij2lem2  9664  ackbij2lem3  9665  divneg  11334  xadddilem  12690  xadddi2  12693  dfceil2  13212  modlt  13251  modmulnn  13260  seqcaopr3  13408  bcval5  13681  hashgadd  13741  hashun3  13748  hashmap  13799  seqcoll  13825  revccat  14130  cshwmodn  14159  2cshwcom  14180  cshimadifsn0  14194  revco  14198  cshco  14200  ofccat  14331  relexpsucl  14394  cjreb  14484  recj  14485  imcj  14493  imval2  14512  sqrtmul  14621  absmax  14691  amgm2  14731  summolem2a  15074  fsumf1o  15082  sumsnf  15101  sumsplit  15125  fsummulc2  15141  binom  15187  bcxmas  15192  incexclem  15193  incexc  15194  expcnv  15221  pwdif  15225  cvgrat  15241  prodmolem3  15289  prodmolem2a  15290  fprodf1o  15302  prodsn  15318  prodsnf  15320  fprodabs  15330  binomfallfac  15397  fallfacval4  15399  bcfallfac  15400  ege2le3  15445  efaddlem  15448  eftlub  15464  tanval3  15489  tanneg  15503  cosmul  15528  cos01bnd  15541  demoivreALT  15556  flodddiv4  15766  absmulgcd  15899  lcmfunsnlem2  15986  eulerthlem2  16121  phisum  16129  pythagtriplem14  16167  pythagtriplem19  16172  pcmul  16190  pcfac  16237  prmreclem6  16259  4sqlem12  16294  vdwlem6  16324  oppccatid  16991  curf2ndf  17499  oppcyon  17521  joincomALT  17641  meetcomALT  17643  pwsco1mhm  17998  sgrp2nmndlem4  18095  qusgrp2  18219  mulgnngsum  18235  mulgnn0p1  18241  mulgneg  18248  mulgnn0dir  18259  qusghm  18397  gaid  18431  symgval  18499  pmtrdifellem3  18608  psgnunilem2  18625  odmulg  18685  sylow1lem2  18726  sylow2a  18746  sylow3lem1  18754  efgredleme  18871  efgcpbllemb  18883  gsumzaddlem  19043  gsumconst  19056  gsumzmhm  19059  ablsimpgfindlem1  19231  srgpcomp  19284  srgbinom  19297  lmodvsmmulgdi  19671  lmodsubdi  19693  rmodislmodlem  19703  0lmhm  19814  lspsneq  19896  qusrhm  20012  quscrng  20015  ascldimulOLD  20119  resspsrmul  20199  evlsscasrng  20312  psropprmul  20408  evls1scasrng  20504  zringlpirlem3  20635  mulgrhm  20647  phssip  20804  frlmip  20924  frlmphl  20927  mat1ghm  21094  mat1mhm  21095  1marepvmarrepid  21186  mdetrlin  21213  mdetrsca2  21215  mdetunilem7  21229  mdetunilem9  21231  mndifsplit  21247  maducoeval2  21251  smadiadetglem2  21283  decpmatmul  21382  pm2mpghm  21426  pm2mpmhmlem2  21429  cpmidgsum2  21489  ptbasfi  22191  ptuni  22204  alexsubALTlem3  22659  subgtgp  22715  tsmsxplem1  22763  xmsusp  23181  restmetu  23182  nminv  23232  nrginvrcnlem  23302  copco  23624  pcoass  23630  pi1bas  23644  pi1xfrf  23659  pi1xfr  23661  isclmp  23703  cph2subdi  23816  cphassr  23818  tcphcphlem1  23840  cphipval  23848  rrxip  23995  rrxnm  23996  pjthlem1  24042  ovolunlem1a  24099  ovolfs2  24174  uniiccdif  24181  ismbf  24231  itgaddlem2  24426  ditgswap  24459  ply1divex  24732  plyeq0lem  24802  plymullem1  24806  dgrcolem1  24865  dgrcolem2  24866  vieta1lem2  24902  elqaalem2  24911  elqaalem3  24912  aaliou3lem7  24940  ulmshft  24980  mulcxplem  25269  cxpmul2  25274  root1eq1  25338  cxpeq  25340  logbchbase  25351  cosangneg2d  25387  isosctrlem2  25399  angpieqvdlem  25408  chordthmlem3  25414  chordthmlem4  25415  chordthmlem5  25416  quad2  25419  dcubic2  25424  cubic2  25428  quart1  25436  scvxcvx  25565  igamlgam  25629  lgam1  25643  basellem9  25668  ppifl  25739  mumul  25760  sgmmul  25779  chtublem  25789  chpub  25798  logfacrlim  25802  dchrsum2  25846  sumdchr2  25848  bposlem9  25870  lgsdir2  25908  lgsdir  25910  lgsdi  25912  lgsdirnn0  25922  lgsdinn0  25923  lgsquad3  25965  2sqblem  26009  chpo1ub  26058  dchrmusum2  26072  dchrvmasumlem1  26073  dchrvmasum2if  26075  dchrisum0fmul  26084  rpvmasum2  26090  mulog2sumlem1  26112  vmalogdivsum2  26116  log2sumbnd  26122  selberg3lem1  26135  selberg4lem1  26138  pntrsumo1  26143  selbergr  26146  pntpbnd1  26164  pntlemk  26184  tgbtwnconn1lem3  26362  mideulem2  26522  axlowdimlem16  26745  axcontlem8  26759  vtxval  26787  iedgval  26788  edgval  26836  vtxdgop  27254  finsumvtxdg2size  27334  lp1cycl  27933  ex-ind-dvds  28242  vsfval  28412  lnocoi  28536  nmblolbii  28578  ipasslem5  28614  hvsubid  28805  sshjval3  29133  pjhthlem1  29170  adjval  29669  unopf1o  29695  kbpj  29735  lnopmi  29779  nmcoplbi  29807  cnlnadjlem2  29847  adjadd  29872  branmfn  29884  pjtoi  29958  ofoprabco  30411  hashxpe  30531  splfv3  30634  xrsmulgzz  30667  psgnfzto1stlem  30744  cycpmco2lem5  30774  cycpmco2lem6  30775  cyc3co2  30784  tocyccntz  30788  cyc3genpmlem  30795  cyc3conja  30801  archiabllem1a  30822  gsumvsca1  30856  gsumvsca2  30857  rdivmuldivd  30864  imaslmod  30924  fedgmullem1  31027  submat1n  31072  submatres  31073  madjusmdetlem3  31096  xrge0iifhom  31182  qqhval2lem  31224  qqhrhm  31232  qqhucn  31235  esumsnf  31325  measvunilem0  31474  carsgclctunlem1  31577  ballotlemfp1  31751  ballotlemsf1o  31773  signstfveq0  31849  breprexplemc  31905  breprexp  31906  breprexpnat  31907  circlemeth  31913  logdivsqrle  31923  hgt750lema  31930  revwlk  32373  cvmlift3lem2  32569  cvmlift3lem4  32571  cvmlift3lem5  32572  cvmlift3lem6  32573  cvmlift3lem9  32576  elmrsubrn  32769  bccolsum  32973  bj-bary1lem  34593  csbdif  34608  finixpnum  34879  poimirlem4  34898  poimirlem16  34910  poimirlem19  34913  poimirlem25  34919  mblfinlem3  34933  dvtan  34944  itg2addnc  34948  itgaddnclem2  34953  ftc1anclem6  34974  areacirclem5  34988  areacirc  34989  upixp  35006  prdsbnd2  35075  ismrer1  35118  rngoneglmul  35223  rngoisocnv  35261  islshpsm  36118  lshpnel2N  36123  lfl0f  36207  ldualvsdi1  36281  ldualgrplem  36283  cmtcomlemN  36386  cvlsupr8  36487  pmodl42N  36989  pmapjat1  36991  llnmod2i2  37001  dalawlem2  37010  pmapj2N  37067  idltrn  37288  cdlemc6  37334  cdleme20d  37450  cdleme22e  37482  cdleme22eALTN  37483  cdleme35b  37588  cdleme48fvg  37638  cdlemg4d  37751  cdlemg8a  37765  cdlemg42  37867  cdlemg47a  37872  tendodi1  37922  tendodi2  37923  cdlemk4  37972  cdlemk21N  38011  cdlemk22  38031  cdlemky  38064  cdlemk53b  38094  cdlemk53  38095  cdlemkyyN  38100  erngdvlem3-rN  38136  tendocnv  38159  dia1dim2  38200  dicvaddcl  38328  dihglblem3N  38433  dihmeetlem4preN  38444  dihmeet2  38484  lcfl7lem  38637  baerlem3lem1  38845  baerlem5alem1  38846  mapdh6bN  38875  mapdh6cN  38876  mapdh6dN  38877  hdmap1l6b  38949  hdmap1l6c  38950  hdmap1l6d  38951  hdmap14lem13  39018  nn0expgcd  39191  3cubeslem2  39289  3cubeslem3r  39291  3cubeslem4  39293  pellexlem2  39434  rmxyneg  39524  oddcomabszz  39548  acongeq  39587  hausgraph  39819  fsovrfovd  40362  inductionexd  40512  expgrowth  40674  binomcxplemwb  40687  binomcxplemnn0  40688  binomcxplemnotnn0  40695  sumsnd  41290  restuni4  41394  fmuldfeqlem1  41870  cncfmptss  41875  climexp  41893  dvresntr  42209  stoweidlem17  42309  wallispi  42362  dirkertrigeq  42393  dirkercncflem2  42396  fourierdlem30  42429  fourierdlem41  42440  fourierdlem81  42479  fourierdlem103  42501  sge0xp  42718  sge0isummpt2  42721  isomennd  42820  vonioolem1  42969  sigarperm  43124  imasetpreimafvbijlemfo  43572  fundcmpsurbijinjpreimafv  43574  fundcmpsurinjimaid  43578  prprspr2  43687  opoeALTV  43855  c0mgm  44187  c0mhm  44188  zrrnghm  44195  cznrng  44233  rngchomrnghmresALTV  44274  fdmdifeqresdif  44397  lincsum  44491  lincscm  44492  lmod1lem4  44552  blennngt2o2  44659  blennn0e2  44661  reccot  44864  rectan  44865  cotsqcscsq  44868  amgmlemALT  44911