Theorem 3eqtr4rd 2776

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 2768	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2768	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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  csbun  4407  csbdif  4490  csbcnvgALT  5851  csbres  5956  fimacnvinrn2  7047  f1ossf1o  7103  suppvalbr  8146  odi  8546  phplem2  9175  cantnfp1lem3  9640  cantnfp1  9641  cardidm  9919  ackbij2lem2  10199  ackbij2lem3  10200  divneg  11881  xadddilem  13261  xadddi2  13264  dfceil2  13808  modlt  13849  modmulnn  13858  seqcaopr3  14009  bcval5  14290  hashgadd  14349  hashun3  14356  hashmap  14407  seqcoll  14436  revccat  14738  cshwmodn  14767  2cshwcom  14788  cshimadifsn0  14803  revco  14807  cshco  14809  ofccat  14942  relexpsucl  15004  dfrtrclrec2  15031  cjreb  15096  recj  15097  imcj  15105  imval2  15124  sqrtmul  15232  absmax  15303  amgm2  15343  summolem2a  15688  fsumf1o  15696  sumsnf  15716  sumsplit  15741  fsummulc2  15757  binom  15803  bcxmas  15808  incexclem  15809  incexc  15810  expcnv  15837  pwdif  15841  cvgrat  15856  prodmolem3  15906  prodmolem2a  15907  fprodf1o  15919  prodsn  15935  prodsnf  15937  fprodabs  15947  binomfallfac  16014  fallfacval4  16016  bcfallfac  16017  ege2le3  16063  efaddlem  16066  eftlub  16084  tanval3  16109  tanneg  16123  cosmul  16148  cos01bnd  16161  demoivreALT  16176  flodddiv4  16392  absmulgcd  16526  nn0expgcd  16541  lcmfunsnlem2  16617  eulerthlem2  16759  phisum  16768  pythagtriplem14  16806  pythagtriplem19  16811  pcmul  16829  pcfac  16877  prmreclem6  16899  4sqlem12  16934  vdwlem6  16964  oppccatid  17687  curf2ndf  18215  oppcyon  18237  joincomALT  18367  meetcomALT  18369  pwsco1mhm  18766  sgrp2nmndlem4  18862  qusgrp2  18997  mulgnngsum  19018  mulgnn0p1  19024  mulgneg  19031  mulgnn0dir  19043  qusghm  19194  gaid  19238  symgval  19308  pmtrdifellem3  19415  psgnunilem2  19432  odmulg  19493  sylow1lem2  19536  sylow2a  19556  sylow3lem1  19564  efgredleme  19680  efgcpbllemb  19692  gsumzaddlem  19858  gsumconst  19871  gsumzmhm  19874  ablsimpgfindlem1  20046  srgpcomp  20134  srgbinom  20147  rdivmuldivd  20329  c0mgm  20375  c0mhm  20376  zrrnghm  20452  imadrhmcl  20713  lmodvsmmulgdi  20810  lmodsubdi  20832  rmodislmodlem  20842  0lmhm  20954  lspsneq  21039  qusrhm  21193  quscrng  21200  zringlpirlem3  21381  mulgrhm  21394  phssip  21574  frlmip  21694  frlmphl  21697  asclmulg  21818  resspsrmul  21892  evlsscasrng  22011  psdadd  22057  psdvsca  22058  psdmul  22060  psdpw  22064  psropprmul  22129  evls1scasrng  22233  mat1ghm  22377  mat1mhm  22378  1marepvmarrepid  22469  mdetrlin  22496  mdetrsca2  22498  mdetunilem7  22512  mdetunilem9  22514  mndifsplit  22530  maducoeval2  22534  smadiadetglem2  22566  decpmatmul  22666  pm2mpghm  22710  pm2mpmhmlem2  22713  cpmidgsum2  22773  ptbasfi  23475  ptuni  23488  alexsubALTlem3  23943  subgtgp  23999  tsmsxplem1  24047  xmsusp  24464  restmetu  24465  nminv  24516  nrginvrcnlem  24586  copco  24925  pcoass  24931  pi1bas  24945  pi1xfrf  24960  pi1xfr  24962  isclmp  25004  cph2subdi  25117  cphassr  25119  tcphcphlem1  25142  cphipval  25150  rrxip  25297  rrxnm  25298  pjthlem1  25344  ovolunlem1a  25404  ovolfs2  25479  uniiccdif  25486  ismbf  25536  itgaddlem2  25732  ditgswap  25767  ply1divex  26049  plyeq0lem  26122  plymullem1  26126  dgrcolem1  26186  dgrcolem2  26187  vieta1lem2  26226  elqaalem2  26235  elqaalem3  26236  aaliou3lem7  26264  ulmshft  26306  mulcxplem  26600  cxpmul2  26605  root1eq1  26672  cxpeq  26674  logbchbase  26688  cosangneg2d  26724  isosctrlem2  26736  angpieqvdlem  26745  chordthmlem3  26751  chordthmlem4  26752  chordthmlem5  26753  quad2  26756  dcubic2  26761  cubic2  26765  quart1  26773  scvxcvx  26903  igamlgam  26967  lgam1  26981  basellem9  27006  ppifl  27077  mumul  27098  sgmmul  27119  chtublem  27129  chpub  27138  logfacrlim  27142  dchrsum2  27186  sumdchr2  27188  bposlem9  27210  lgsdir2  27248  lgsdir  27250  lgsdi  27252  lgsdirnn0  27262  lgsdinn0  27263  lgsquad3  27305  2sqblem  27349  chpo1ub  27398  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2if  27415  dchrisum0fmul  27424  rpvmasum2  27430  mulog2sumlem1  27452  vmalogdivsum2  27456  log2sumbnd  27462  selberg3lem1  27475  selberg4lem1  27478  pntrsumo1  27483  selbergr  27486  pntpbnd1  27504  pntlemk  27524  mulsunif2lem  28079  divsasswd  28113  absmuls  28153  eucliddivs  28272  zscut  28302  expsp1  28322  expadds  28327  pw2divsrecd  28337  tgbtwnconn1lem3  28508  mideulem2  28668  axlowdimlem16  28891  axcontlem8  28905  vtxval  28934  iedgval  28935  edgval  28983  vtxdgop  29405  finsumvtxdg2size  29485  lp1cycl  30088  ex-ind-dvds  30397  vsfval  30569  lnocoi  30693  nmblolbii  30735  ipasslem5  30771  hvsubid  30962  sshjval3  31290  pjhthlem1  31327  adjval  31826  unopf1o  31852  kbpj  31892  lnopmi  31936  nmcoplbi  31964  cnlnadjlem2  32004  adjadd  32029  branmfn  32041  pjtoi  32115  ofoprabco  32595  supppreima  32621  sgnval2  32665  hashxpe  32739  ccatws1f1o  32880  splfv3  32887  xrsmulgzz  32954  mndractfo  32977  mndlactf1o  32978  mndractf1o  32979  gsumfs2d  33002  psgnfzto1stlem  33064  cycpmco2lem5  33094  cycpmco2lem6  33095  cyc3co2  33104  tocyccntz  33108  cyc3genpmlem  33115  cyc3conja  33121  archiabllem1a  33152  gsumvsca1  33186  gsumvsca2  33187  elrgspnlem2  33201  elrgspnsubrunlem1  33205  rloccring  33228  imaslmod  33331  elrspunidl  33406  mxidlirredi  33449  opprabs  33460  qsdrngi  33473  1arithidomlem1  33513  1arithidomlem2  33514  zringfrac  33532  ressply1evls1  33541  ply1degltdimlem  33625  fedgmullem1  33632  fldextrspunlsplem  33675  algextdeglem4  33717  constrconj  33742  constrdircl  33762  constrremulcl  33764  constrimcl  33767  constrresqrtcl  33774  cos9thpiminplylem2  33780  submat1n  33802  submatres  33803  madjusmdetlem3  33826  xrge0iifhom  33934  qqhval2lem  33978  qqhrhm  33986  qqhucn  33989  esumsnf  34061  measvunilem0  34210  carsgclctunlem1  34315  ballotlemfp1  34490  ballotlemsf1o  34512  signstfveq0  34575  breprexplemc  34630  breprexp  34631  breprexpnat  34632  circlemeth  34638  logdivsqrle  34648  hgt750lema  34655  revwlk  35119  cvmlift3lem2  35314  cvmlift3lem4  35316  cvmlift3lem5  35317  cvmlift3lem6  35318  cvmlift3lem9  35321  elmrsubrn  35514  bccolsum  35733  bj-bary1lem  37305  finixpnum  37606  poimirlem4  37625  poimirlem16  37637  poimirlem19  37640  poimirlem25  37646  mblfinlem3  37660  dvtan  37671  itg2addnc  37675  itgaddnclem2  37680  ftc1anclem6  37699  areacirclem5  37713  areacirc  37714  upixp  37730  prdsbnd2  37796  ismrer1  37839  rngoneglmul  37944  rngoisocnv  37982  islshpsm  38980  lshpnel2N  38985  lfl0f  39069  ldualvsdi1  39143  ldualgrplem  39145  cmtcomlemN  39248  cvlsupr8  39349  pmodl42N  39852  pmapjat1  39854  llnmod2i2  39864  dalawlem2  39873  pmapj2N  39930  idltrn  40151  cdlemc6  40197  cdleme20d  40313  cdleme22e  40345  cdleme22eALTN  40346  cdleme35b  40451  cdleme48fvg  40501  cdlemg4d  40614  cdlemg8a  40628  cdlemg42  40730  cdlemg47a  40735  tendodi1  40785  tendodi2  40786  cdlemk4  40835  cdlemk21N  40874  cdlemk22  40894  cdlemky  40927  cdlemk53b  40957  cdlemk53  40958  cdlemkyyN  40963  erngdvlem3-rN  40999  tendocnv  41022  dia1dim2  41063  dicvaddcl  41191  dihglblem3N  41296  dihmeetlem4preN  41307  dihmeet2  41347  lcfl7lem  41500  baerlem3lem1  41708  baerlem5alem1  41709  mapdh6bN  41738  mapdh6cN  41739  mapdh6dN  41740  hdmap1l6b  41812  hdmap1l6c  41813  hdmap1l6d  41814  hdmap14lem13  41881  ofun  42231  grpcominv1  42503  evlselv  42582  flt4lem7  42654  3cubeslem2  42680  3cubeslem3r  42682  3cubeslem4  42684  pellexlem2  42825  rmxyneg  42916  oddcomabszz  42940  acongeq  42979  hausgraph  43201  onsupnmax  43224  tfsconcatrev  43344  naddass1  43389  fsovrfovd  44005  inductionexd  44151  expgrowth  44331  binomcxplemwb  44344  binomcxplemnn0  44345  binomcxplemnotnn0  44352  sumsnd  45027  restuni4  45122  fmuldfeqlem1  45587  cncfmptss  45592  climexp  45610  dvresntr  45923  stoweidlem17  46022  wallispi  46075  dirkertrigeq  46106  dirkercncflem2  46109  fourierdlem30  46142  fourierdlem41  46153  fourierdlem81  46192  fourierdlem103  46214  sge0xp  46434  sge0isummpt2  46437  isomennd  46536  vonioolem1  46685  sigarperm  46865  fcores  47072  imasetpreimafvbijlemfo  47410  fundcmpsurbijinjpreimafv  47412  fundcmpsurinjimaid  47416  prprspr2  47523  opoeALTV  47688  uhgrimisgrgric  47935  isubgr3stgrlem2  47970  cznrng  48253  rngchomrnghmresALTV  48271  fdmdifeqresdif  48334  lincsum  48422  lincscm  48423  lmod1lem4  48483  blennngt2o2  48585  blennn0e2  48587  tposideq  48880  topdlat  48996  sectpropdlem  49029  invpropdlem  49031  isopropdlem  49033  imaidfu  49103  imasubc  49144  natoppf  49222  swapfid  49272  swapfcoa  49274  fucoppcid  49401  fucoppcco  49402  oppfdiag1  49407  diag1f1olem  49526  oppgoppchom  49583  oppgoppcco  49584  oppgoppcid  49585  2arwcat  49593  reccot  49751  rectan  49752  cotsqcscsq  49755  amgmlemALT  49796