Theorem 3eqtr4rd 2783

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  csbun  4395  csbdif  4480  csbcnvgALT  5841  csbres  5949  fimacnvinrn2  7026  f1ossf1o  7083  suppvalbr  8116  odi  8516  phplem2  9141  cantnfp1lem3  9601  cantnfp1  9602  cardidm  9883  ackbij2lem2  10161  ackbij2lem3  10162  divneg  11845  xadddilem  13221  xadddi2  13224  dfceil2  13771  modlt  13812  modmulnn  13821  seqcaopr3  13972  bcval5  14253  hashgadd  14312  hashun3  14319  hashmap  14370  seqcoll  14399  revccat  14701  cshwmodn  14730  2cshwcom  14751  cshimadifsn0  14765  revco  14769  cshco  14771  ofccat  14904  relexpsucl  14966  dfrtrclrec2  14993  cjreb  15058  recj  15059  imcj  15067  imval2  15086  sqrtmul  15194  absmax  15265  amgm2  15305  summolem2a  15650  fsumf1o  15658  sumsnf  15678  sumsplit  15703  fsummulc2  15719  binom  15765  bcxmas  15770  incexclem  15771  incexc  15772  expcnv  15799  pwdif  15803  cvgrat  15818  prodmolem3  15868  prodmolem2a  15869  fprodf1o  15881  prodsn  15897  prodsnf  15899  fprodabs  15909  binomfallfac  15976  fallfacval4  15978  bcfallfac  15979  ege2le3  16025  efaddlem  16028  eftlub  16046  tanval3  16071  tanneg  16085  cosmul  16110  cos01bnd  16123  demoivreALT  16138  flodddiv4  16354  absmulgcd  16488  nn0expgcd  16503  lcmfunsnlem2  16579  eulerthlem2  16721  phisum  16730  pythagtriplem14  16768  pythagtriplem19  16773  pcmul  16791  pcfac  16839  prmreclem6  16861  4sqlem12  16896  vdwlem6  16926  oppccatid  17654  curf2ndf  18182  oppcyon  18204  joincomALT  18334  meetcomALT  18336  pwsco1mhm  18769  sgrp2nmndlem4  18868  qusgrp2  19003  mulgnngsum  19024  mulgnn0p1  19030  mulgneg  19037  mulgnn0dir  19049  qusghm  19199  gaid  19243  symgval  19315  pmtrdifellem3  19422  psgnunilem2  19439  odmulg  19500  sylow1lem2  19543  sylow2a  19563  sylow3lem1  19571  efgredleme  19687  efgcpbllemb  19699  gsumzaddlem  19865  gsumconst  19878  gsumzmhm  19881  ablsimpgfindlem1  20053  srgpcomp  20168  srgbinom  20181  rdivmuldivd  20364  c0mgm  20410  c0mhm  20411  zrrnghm  20484  imadrhmcl  20745  lmodvsmmulgdi  20863  lmodsubdi  20885  rmodislmodlem  20895  0lmhm  21007  lspsneq  21092  qusrhm  21246  quscrng  21253  zringlpirlem3  21434  mulgrhm  21447  phssip  21628  frlmip  21748  frlmphl  21751  asclmulg  21873  resspsrmul  21946  evlsscasrng  22075  psdadd  22121  psdvsca  22122  psdmul  22124  psdpw  22128  psropprmul  22193  evls1scasrng  22298  mat1ghm  22442  mat1mhm  22443  1marepvmarrepid  22534  mdetrlin  22561  mdetrsca2  22563  mdetunilem7  22577  mdetunilem9  22579  mndifsplit  22595  maducoeval2  22599  smadiadetglem2  22631  decpmatmul  22731  pm2mpghm  22775  pm2mpmhmlem2  22778  cpmidgsum2  22838  ptbasfi  23540  ptuni  23553  alexsubALTlem3  24008  subgtgp  24064  tsmsxplem1  24112  xmsusp  24528  restmetu  24529  nminv  24580  nrginvrcnlem  24650  copco  24989  pcoass  24995  pi1bas  25009  pi1xfrf  25024  pi1xfr  25026  isclmp  25068  cph2subdi  25181  cphassr  25183  tcphcphlem1  25206  cphipval  25214  rrxip  25361  rrxnm  25362  pjthlem1  25408  ovolunlem1a  25468  ovolfs2  25543  uniiccdif  25550  ismbf  25600  itgaddlem2  25796  ditgswap  25831  ply1divex  26113  plyeq0lem  26186  plymullem1  26190  dgrcolem1  26250  dgrcolem2  26251  vieta1lem2  26290  elqaalem2  26299  elqaalem3  26300  aaliou3lem7  26328  ulmshft  26370  mulcxplem  26664  cxpmul2  26669  root1eq1  26736  cxpeq  26738  logbchbase  26752  cosangneg2d  26788  isosctrlem2  26800  angpieqvdlem  26809  chordthmlem3  26815  chordthmlem4  26816  chordthmlem5  26817  quad2  26820  dcubic2  26825  cubic2  26829  quart1  26837  scvxcvx  26967  igamlgam  27031  lgam1  27045  basellem9  27070  ppifl  27141  mumul  27162  sgmmul  27183  chtublem  27193  chpub  27202  logfacrlim  27206  dchrsum2  27250  sumdchr2  27252  bposlem9  27274  lgsdir2  27312  lgsdir  27314  lgsdi  27316  lgsdirnn0  27326  lgsdinn0  27327  lgsquad3  27369  2sqblem  27413  chpo1ub  27462  dchrmusum2  27476  dchrvmasumlem1  27477  dchrvmasum2if  27479  dchrisum0fmul  27488  rpvmasum2  27494  mulog2sumlem1  27516  vmalogdivsum2  27520  log2sumbnd  27526  selberg3lem1  27539  selberg4lem1  27542  pntrsumo1  27547  selbergr  27550  pntpbnd1  27568  pntlemk  27588  lesubsd  28107  mulsunif2lem  28180  divsasswd  28214  absmuls  28255  eucliddivs  28387  zcuts  28418  expsp1  28440  expadds  28446  pw2divsrecd  28458  pw2cut2  28473  bdayfinbndlem1  28478  tgbtwnconn1lem3  28662  mideulem2  28822  axlowdimlem16  29046  axcontlem8  29060  vtxval  29089  iedgval  29090  edgval  29138  vtxdgop  29560  finsumvtxdg2size  29640  lp1cycl  30243  ex-ind-dvds  30552  vsfval  30725  lnocoi  30849  nmblolbii  30891  ipasslem5  30927  hvsubid  31118  sshjval3  31446  pjhthlem1  31483  adjval  31982  unopf1o  32008  kbpj  32048  lnopmi  32092  nmcoplbi  32120  cnlnadjlem2  32160  adjadd  32185  branmfn  32197  pjtoi  32271  fconst7v  32714  ofoprabco  32758  supppreima  32785  sgnval2  32829  hashxpe  32902  ccatws1f1o  33048  splfv3  33055  xrsmulgzz  33106  mndractfo  33126  mndlactf1o  33127  mndractf1o  33128  gsumfs2d  33159  psgnfzto1stlem  33198  cycpmco2lem5  33228  cycpmco2lem6  33229  cyc3co2  33238  tocyccntz  33242  cyc3genpmlem  33249  cyc3conja  33255  archiabllem1a  33289  gsumvsca1  33324  gsumvsca2  33325  elrgspnlem2  33341  elrgspnsubrunlem1  33345  rloccring  33368  imaslmod  33450  elrspunidl  33525  mxidlirredi  33568  opprabs  33579  qsdrngi  33592  1arithidomlem1  33632  1arithidomlem2  33633  zringfrac  33651  ressply1evls1  33662  deg1prod  33680  psrbasfsupp  33709  mplvrpmga  33726  esplyind  33756  vietalem  33760  vieta  33761  ply1degltdimlem  33804  fedgmullem1  33811  fldextrspunlsplem  33855  extdgfialglem2  33875  algextdeglem4  33902  constrconj  33927  constrdircl  33947  constrremulcl  33949  constrimcl  33952  constrresqrtcl  33959  cos9thpiminplylem2  33965  submat1n  33987  submatres  33988  madjusmdetlem3  34011  xrge0iifhom  34119  qqhval2lem  34163  qqhrhm  34171  qqhucn  34174  esumsnf  34246  measvunilem0  34395  carsgclctunlem1  34499  ballotlemfp1  34674  ballotlemsf1o  34696  signstfveq0  34759  breprexplemc  34814  breprexp  34815  breprexpnat  34816  circlemeth  34822  logdivsqrle  34832  hgt750lema  34839  revwlk  35345  cvmlift3lem2  35540  cvmlift3lem4  35542  cvmlift3lem5  35543  cvmlift3lem6  35544  cvmlift3lem9  35547  elmrsubrn  35740  bccolsum  35959  bj-bary1lem  37569  finixpnum  37860  poimirlem4  37879  poimirlem16  37891  poimirlem19  37894  poimirlem25  37900  mblfinlem3  37914  dvtan  37925  itg2addnc  37929  itgaddnclem2  37934  ftc1anclem6  37953  areacirclem5  37967  areacirc  37968  upixp  37984  prdsbnd2  38050  ismrer1  38093  rngoneglmul  38198  rngoisocnv  38236  ecun  38648  islshpsm  39360  lshpnel2N  39365  lfl0f  39449  ldualvsdi1  39523  ldualgrplem  39525  cmtcomlemN  39628  cvlsupr8  39729  pmodl42N  40231  pmapjat1  40233  llnmod2i2  40243  dalawlem2  40252  pmapj2N  40309  idltrn  40530  cdlemc6  40576  cdleme20d  40692  cdleme22e  40724  cdleme22eALTN  40725  cdleme35b  40830  cdleme48fvg  40880  cdlemg4d  40993  cdlemg8a  41007  cdlemg42  41109  cdlemg47a  41114  tendodi1  41164  tendodi2  41165  cdlemk4  41214  cdlemk21N  41253  cdlemk22  41273  cdlemky  41306  cdlemk53b  41336  cdlemk53  41337  cdlemkyyN  41342  erngdvlem3-rN  41378  tendocnv  41401  dia1dim2  41442  dicvaddcl  41570  dihglblem3N  41675  dihmeetlem4preN  41686  dihmeet2  41726  lcfl7lem  41879  baerlem3lem1  42087  baerlem5alem1  42088  mapdh6bN  42117  mapdh6cN  42118  mapdh6dN  42119  hdmap1l6b  42191  hdmap1l6c  42192  hdmap1l6d  42193  hdmap14lem13  42260  ofun  42612  grpcominv1  42882  evlselv  42949  flt4lem7  43021  3cubeslem2  43046  3cubeslem3r  43048  3cubeslem4  43050  pellexlem2  43191  rmxyneg  43281  oddcomabszz  43305  acongeq  43344  hausgraph  43566  onsupnmax  43589  tfsconcatrev  43709  naddass1  43754  fsovrfovd  44369  inductionexd  44515  expgrowth  44695  binomcxplemwb  44708  binomcxplemnn0  44709  binomcxplemnotnn0  44716  sumsnd  45390  restuni4  45484  fmuldfeqlem1  45946  cncfmptss  45951  climexp  45969  dvresntr  46280  stoweidlem17  46379  wallispi  46432  dirkertrigeq  46463  dirkercncflem2  46466  fourierdlem30  46499  fourierdlem41  46510  fourierdlem81  46549  fourierdlem103  46571  sge0xp  46791  sge0isummpt2  46794  isomennd  46893  vonioolem1  47042  sigarperm  47222  fcores  47431  imasetpreimafvbijlemfo  47769  fundcmpsurbijinjpreimafv  47771  fundcmpsurinjimaid  47775  prprspr2  47882  opoeALTV  48047  uhgrimisgrgric  48295  isubgr3stgrlem2  48331  cznrng  48625  rngchomrnghmresALTV  48643  fdmdifeqresdif  48706  lincsum  48793  lincscm  48794  lmod1lem4  48854  blennngt2o2  48956  blennn0e2  48958  tposideq  49251  topdlat  49367  sectpropdlem  49399  invpropdlem  49401  isopropdlem  49403  imaidfu  49473  imasubc  49514  natoppf  49592  swapfid  49642  swapfcoa  49644  fucoppcid  49771  fucoppcco  49772  oppfdiag1  49777  diag1f1olem  49896  oppgoppchom  49953  oppgoppcco  49954  oppgoppcid  49955  2arwcat  49963  reccot  50121  rectan  50122  cotsqcscsq  50125  amgmlemALT  50166