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 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  csbun  4437  csbdif  4526  csbcnvgALT  5882  csbres  5982  fimacnvinrn2  7071  f1ossf1o  7122  suppvalbr  8146  odi  8575  phplem2  9204  phplem4OLD  9216  cantnfp1lem3  9671  cantnfp1  9672  cardidm  9950  ackbij2lem2  10231  ackbij2lem3  10232  divneg  11902  xadddilem  13269  xadddi2  13272  dfceil2  13800  modlt  13841  modmulnn  13850  seqcaopr3  13999  bcval5  14274  hashgadd  14333  hashun3  14340  hashmap  14391  seqcoll  14421  revccat  14712  cshwmodn  14741  2cshwcom  14762  cshimadifsn0  14777  revco  14781  cshco  14783  ofccat  14912  relexpsucl  14974  dfrtrclrec2  15001  cjreb  15066  recj  15067  imcj  15075  imval2  15094  sqrtmul  15202  absmax  15272  amgm2  15312  summolem2a  15657  fsumf1o  15665  sumsnf  15685  sumsplit  15710  fsummulc2  15726  binom  15772  bcxmas  15777  incexclem  15778  incexc  15779  expcnv  15806  pwdif  15810  cvgrat  15825  prodmolem3  15873  prodmolem2a  15874  fprodf1o  15886  prodsn  15902  prodsnf  15904  fprodabs  15914  binomfallfac  15981  fallfacval4  15983  bcfallfac  15984  ege2le3  16029  efaddlem  16032  eftlub  16048  tanval3  16073  tanneg  16087  cosmul  16112  cos01bnd  16125  demoivreALT  16140  flodddiv4  16352  absmulgcd  16487  lcmfunsnlem2  16573  eulerthlem2  16711  phisum  16719  pythagtriplem14  16757  pythagtriplem19  16762  pcmul  16780  pcfac  16828  prmreclem6  16850  4sqlem12  16885  vdwlem6  16915  oppccatid  17661  curf2ndf  18196  oppcyon  18218  joincomALT  18350  meetcomALT  18352  pwsco1mhm  18709  sgrp2nmndlem4  18805  qusgrp2  18937  mulgnngsum  18953  mulgnn0p1  18959  mulgneg  18966  mulgnn0dir  18978  qusghm  19123  gaid  19157  symgval  19230  pmtrdifellem3  19340  psgnunilem2  19357  odmulg  19418  sylow1lem2  19461  sylow2a  19481  sylow3lem1  19489  efgredleme  19605  efgcpbllemb  19617  gsumzaddlem  19783  gsumconst  19796  gsumzmhm  19799  ablsimpgfindlem1  19971  srgpcomp  20034  srgbinom  20047  rdivmuldivd  20219  imadrhmcl  20405  lmodvsmmulgdi  20499  lmodsubdi  20521  rmodislmodlem  20531  0lmhm  20643  lspsneq  20727  qusrhm  20866  quscrng  20870  zringlpirlem3  21025  mulgrhm  21038  phssip  21202  frlmip  21324  frlmphl  21327  resspsrmul  21528  evlsscasrng  21651  psropprmul  21751  evls1scasrng  21849  mat1ghm  21976  mat1mhm  21977  1marepvmarrepid  22068  mdetrlin  22095  mdetrsca2  22097  mdetunilem7  22111  mdetunilem9  22113  mndifsplit  22129  maducoeval2  22133  smadiadetglem2  22165  decpmatmul  22265  pm2mpghm  22309  pm2mpmhmlem2  22312  cpmidgsum2  22372  ptbasfi  23076  ptuni  23089  alexsubALTlem3  23544  subgtgp  23600  tsmsxplem1  23648  xmsusp  24069  restmetu  24070  nminv  24121  nrginvrcnlem  24199  copco  24525  pcoass  24531  pi1bas  24545  pi1xfrf  24560  pi1xfr  24562  isclmp  24604  cph2subdi  24718  cphassr  24720  tcphcphlem1  24743  cphipval  24751  rrxip  24898  rrxnm  24899  pjthlem1  24945  ovolunlem1a  25004  ovolfs2  25079  uniiccdif  25086  ismbf  25136  itgaddlem2  25332  ditgswap  25367  ply1divex  25645  plyeq0lem  25715  plymullem1  25719  dgrcolem1  25778  dgrcolem2  25779  vieta1lem2  25815  elqaalem2  25824  elqaalem3  25825  aaliou3lem7  25853  ulmshft  25893  mulcxplem  26183  cxpmul2  26188  root1eq1  26252  cxpeq  26254  logbchbase  26265  cosangneg2d  26301  isosctrlem2  26313  angpieqvdlem  26322  chordthmlem3  26328  chordthmlem4  26329  chordthmlem5  26330  quad2  26333  dcubic2  26338  cubic2  26342  quart1  26350  scvxcvx  26479  igamlgam  26543  lgam1  26557  basellem9  26582  ppifl  26653  mumul  26674  sgmmul  26693  chtublem  26703  chpub  26712  logfacrlim  26716  dchrsum2  26760  sumdchr2  26762  bposlem9  26784  lgsdir2  26822  lgsdir  26824  lgsdi  26826  lgsdirnn0  26836  lgsdinn0  26837  lgsquad3  26879  2sqblem  26923  chpo1ub  26972  dchrmusum2  26986  dchrvmasumlem1  26987  dchrvmasum2if  26989  dchrisum0fmul  26998  rpvmasum2  27004  mulog2sumlem1  27026  vmalogdivsum2  27030  log2sumbnd  27036  selberg3lem1  27049  selberg4lem1  27052  pntrsumo1  27057  selbergr  27060  pntpbnd1  27078  pntlemk  27098  divsasswd  27639  tgbtwnconn1lem3  27814  mideulem2  27974  axlowdimlem16  28204  axcontlem8  28218  vtxval  28249  iedgval  28250  edgval  28298  vtxdgop  28716  finsumvtxdg2size  28796  lp1cycl  29394  ex-ind-dvds  29703  vsfval  29873  lnocoi  29997  nmblolbii  30039  ipasslem5  30075  hvsubid  30266  sshjval3  30594  pjhthlem1  30631  adjval  31130  unopf1o  31156  kbpj  31196  lnopmi  31240  nmcoplbi  31268  cnlnadjlem2  31308  adjadd  31333  branmfn  31345  pjtoi  31419  ofoprabco  31876  supppreima  31900  hashxpe  32006  splfv3  32109  xrsmulgzz  32166  psgnfzto1stlem  32246  cycpmco2lem5  32276  cycpmco2lem6  32277  cyc3co2  32286  tocyccntz  32290  cyc3genpmlem  32297  cyc3conja  32303  archiabllem1a  32324  gsumvsca1  32358  gsumvsca2  32359  imaslmod  32456  elrspunidl  32534  mxidlirredi  32575  opprabs  32584  qsdrngi  32597  asclmulg  32623  ply1degltdimlem  32695  fedgmullem1  32702  algextdeglem1  32760  submat1n  32773  submatres  32774  madjusmdetlem3  32797  xrge0iifhom  32905  qqhval2lem  32949  qqhrhm  32957  qqhucn  32960  esumsnf  33050  measvunilem0  33199  carsgclctunlem1  33304  ballotlemfp1  33478  ballotlemsf1o  33500  signstfveq0  33576  breprexplemc  33632  breprexp  33633  breprexpnat  33634  circlemeth  33640  logdivsqrle  33650  hgt750lema  33657  revwlk  34103  cvmlift3lem2  34299  cvmlift3lem4  34301  cvmlift3lem5  34302  cvmlift3lem6  34303  cvmlift3lem9  34306  elmrsubrn  34499  bccolsum  34697  bj-bary1lem  36179  finixpnum  36461  poimirlem4  36480  poimirlem16  36492  poimirlem19  36495  poimirlem25  36501  mblfinlem3  36515  dvtan  36526  itg2addnc  36530  itgaddnclem2  36535  ftc1anclem6  36554  areacirclem5  36568  areacirc  36569  upixp  36585  prdsbnd2  36651  ismrer1  36694  rngoneglmul  36799  rngoisocnv  36837  islshpsm  37838  lshpnel2N  37843  lfl0f  37927  ldualvsdi1  38001  ldualgrplem  38003  cmtcomlemN  38106  cvlsupr8  38207  pmodl42N  38710  pmapjat1  38712  llnmod2i2  38722  dalawlem2  38731  pmapj2N  38788  idltrn  39009  cdlemc6  39055  cdleme20d  39171  cdleme22e  39203  cdleme22eALTN  39204  cdleme35b  39309  cdleme48fvg  39359  cdlemg4d  39472  cdlemg8a  39486  cdlemg42  39588  cdlemg47a  39593  tendodi1  39643  tendodi2  39644  cdlemk4  39693  cdlemk21N  39732  cdlemk22  39752  cdlemky  39785  cdlemk53b  39815  cdlemk53  39816  cdlemkyyN  39821  erngdvlem3-rN  39857  tendocnv  39880  dia1dim2  39921  dicvaddcl  40049  dihglblem3N  40154  dihmeetlem4preN  40165  dihmeet2  40205  lcfl7lem  40358  baerlem3lem1  40566  baerlem5alem1  40567  mapdh6bN  40596  mapdh6cN  40597  mapdh6dN  40598  hdmap1l6b  40670  hdmap1l6c  40671  hdmap1l6d  40672  hdmap14lem13  40739  ofun  41055  grpcominv1  41079  evlselv  41156  nn0expgcd  41221  flt4lem7  41397  3cubeslem2  41408  3cubeslem3r  41410  3cubeslem4  41412  pellexlem2  41553  rmxyneg  41644  oddcomabszz  41668  acongeq  41707  hausgraph  41939  onsupnmax  41962  tfsconcatrev  42083  naddass1  42129  fsovrfovd  42745  inductionexd  42891  expgrowth  43079  binomcxplemwb  43092  binomcxplemnn0  43093  binomcxplemnotnn0  43100  sumsnd  43695  restuni4  43795  fmuldfeqlem1  44284  cncfmptss  44289  climexp  44307  dvresntr  44620  stoweidlem17  44719  wallispi  44772  dirkertrigeq  44803  dirkercncflem2  44806  fourierdlem30  44839  fourierdlem41  44850  fourierdlem81  44889  fourierdlem103  44911  sge0xp  45131  sge0isummpt2  45134  isomennd  45233  vonioolem1  45382  sigarperm  45562  fcores  45763  imasetpreimafvbijlemfo  46059  fundcmpsurbijinjpreimafv  46061  fundcmpsurinjimaid  46065  prprspr2  46172  opoeALTV  46337  c0mgm  46693  c0mhm  46694  zrrnghm  46701  cznrng  46806  rngchomrnghmresALTV  46847  fdmdifeqresdif  46970  lincsum  47063  lincscm  47064  lmod1lem4  47124  blennngt2o2  47231  blennn0e2  47233  topdlat  47582  reccot  47756  rectan  47757  cotsqcscsq  47760  amgmlemALT  47803