Theorem 3eqtr4rd 2787

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 2779	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2779	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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2728

This theorem is referenced by:  csbun  4386  csbdif  4473  csbcnvgALT  5827  csbres  5927  fimacnvinrn2  7007  f1ossf1o  7057  odi  8482  phplem2  9074  phplem4OLD  9086  cantnfp1lem3  9538  cantnfp1  9539  cardidm  9817  ackbij2lem2  10098  ackbij2lem3  10099  divneg  11769  xadddilem  13130  xadddi2  13133  dfceil2  13661  modlt  13702  modmulnn  13711  seqcaopr3  13860  bcval5  14134  hashgadd  14193  hashun3  14200  hashmap  14251  seqcoll  14279  revccat  14578  cshwmodn  14607  2cshwcom  14628  cshimadifsn0  14643  revco  14647  cshco  14649  ofccat  14780  relexpsucl  14842  dfrtrclrec2  14869  cjreb  14934  recj  14935  imcj  14943  imval2  14962  sqrtmul  15071  absmax  15141  amgm2  15181  summolem2a  15527  fsumf1o  15535  sumsnf  15555  sumsplit  15580  fsummulc2  15596  binom  15642  bcxmas  15647  incexclem  15648  incexc  15649  expcnv  15676  pwdif  15680  cvgrat  15695  prodmolem3  15743  prodmolem2a  15744  fprodf1o  15756  prodsn  15772  prodsnf  15774  fprodabs  15784  binomfallfac  15851  fallfacval4  15853  bcfallfac  15854  ege2le3  15899  efaddlem  15902  eftlub  15918  tanval3  15943  tanneg  15957  cosmul  15982  cos01bnd  15995  demoivreALT  16010  flodddiv4  16222  absmulgcd  16357  lcmfunsnlem2  16443  eulerthlem2  16581  phisum  16589  pythagtriplem14  16627  pythagtriplem19  16632  pcmul  16650  pcfac  16698  prmreclem6  16720  4sqlem12  16755  vdwlem6  16785  oppccatid  17528  curf2ndf  18063  oppcyon  18085  joincomALT  18217  meetcomALT  18219  pwsco1mhm  18568  sgrp2nmndlem4  18664  qusgrp2  18790  mulgnngsum  18806  mulgnn0p1  18812  mulgneg  18819  mulgnn0dir  18830  qusghm  18968  gaid  19002  symgval  19073  pmtrdifellem3  19183  psgnunilem2  19200  odmulg  19260  sylow1lem2  19301  sylow2a  19321  sylow3lem1  19329  efgredleme  19445  efgcpbllemb  19457  gsumzaddlem  19618  gsumconst  19631  gsumzmhm  19634  ablsimpgfindlem1  19806  srgpcomp  19864  srgbinom  19877  lmodvsmmulgdi  20265  lmodsubdi  20287  rmodislmodlem  20297  0lmhm  20409  lspsneq  20491  qusrhm  20615  quscrng  20618  zringlpirlem3  20793  mulgrhm  20806  phssip  20970  frlmip  21092  frlmphl  21095  resspsrmul  21293  evlsscasrng  21414  psropprmul  21516  evls1scasrng  21612  mat1ghm  21739  mat1mhm  21740  1marepvmarrepid  21831  mdetrlin  21858  mdetrsca2  21860  mdetunilem7  21874  mdetunilem9  21876  mndifsplit  21892  maducoeval2  21896  smadiadetglem2  21928  decpmatmul  22028  pm2mpghm  22072  pm2mpmhmlem2  22075  cpmidgsum2  22135  ptbasfi  22839  ptuni  22852  alexsubALTlem3  23307  subgtgp  23363  tsmsxplem1  23411  xmsusp  23832  restmetu  23833  nminv  23884  nrginvrcnlem  23962  copco  24288  pcoass  24294  pi1bas  24308  pi1xfrf  24323  pi1xfr  24325  isclmp  24367  cph2subdi  24481  cphassr  24483  tcphcphlem1  24506  cphipval  24514  rrxip  24661  rrxnm  24662  pjthlem1  24708  ovolunlem1a  24767  ovolfs2  24842  uniiccdif  24849  ismbf  24899  itgaddlem2  25095  ditgswap  25130  ply1divex  25408  plyeq0lem  25478  plymullem1  25482  dgrcolem1  25541  dgrcolem2  25542  vieta1lem2  25578  elqaalem2  25587  elqaalem3  25588  aaliou3lem7  25616  ulmshft  25656  mulcxplem  25946  cxpmul2  25951  root1eq1  26015  cxpeq  26017  logbchbase  26028  cosangneg2d  26064  isosctrlem2  26076  angpieqvdlem  26085  chordthmlem3  26091  chordthmlem4  26092  chordthmlem5  26093  quad2  26096  dcubic2  26101  cubic2  26105  quart1  26113  scvxcvx  26242  igamlgam  26306  lgam1  26320  basellem9  26345  ppifl  26416  mumul  26437  sgmmul  26456  chtublem  26466  chpub  26475  logfacrlim  26479  dchrsum2  26523  sumdchr2  26525  bposlem9  26547  lgsdir2  26585  lgsdir  26587  lgsdi  26589  lgsdirnn0  26599  lgsdinn0  26600  lgsquad3  26642  2sqblem  26686  chpo1ub  26735  dchrmusum2  26749  dchrvmasumlem1  26750  dchrvmasum2if  26752  dchrisum0fmul  26761  rpvmasum2  26767  mulog2sumlem1  26789  vmalogdivsum2  26793  log2sumbnd  26799  selberg3lem1  26812  selberg4lem1  26815  pntrsumo1  26820  selbergr  26823  pntpbnd1  26841  pntlemk  26861  tgbtwnconn1lem3  27225  mideulem2  27385  axlowdimlem16  27615  axcontlem8  27629  vtxval  27660  iedgval  27661  edgval  27709  vtxdgop  28127  finsumvtxdg2size  28207  lp1cycl  28805  ex-ind-dvds  29114  vsfval  29284  lnocoi  29408  nmblolbii  29450  ipasslem5  29486  hvsubid  29677  sshjval3  30005  pjhthlem1  30042  adjval  30541  unopf1o  30567  kbpj  30607  lnopmi  30651  nmcoplbi  30679  cnlnadjlem2  30719  adjadd  30744  branmfn  30756  pjtoi  30830  ofoprabco  31288  supppreima  31312  hashxpe  31414  splfv3  31517  xrsmulgzz  31574  psgnfzto1stlem  31654  cycpmco2lem5  31684  cycpmco2lem6  31685  cyc3co2  31694  tocyccntz  31698  cyc3genpmlem  31705  cyc3conja  31711  archiabllem1a  31732  gsumvsca1  31766  gsumvsca2  31767  rdivmuldivd  31775  imaslmod  31849  elrspunidl  31903  asclmulg  31963  fedgmullem1  32008  submat1n  32053  submatres  32054  madjusmdetlem3  32077  xrge0iifhom  32185  qqhval2lem  32229  qqhrhm  32237  qqhucn  32240  esumsnf  32330  measvunilem0  32479  carsgclctunlem1  32584  ballotlemfp1  32758  ballotlemsf1o  32780  signstfveq0  32856  breprexplemc  32912  breprexp  32913  breprexpnat  32914  circlemeth  32920  logdivsqrle  32930  hgt750lema  32937  revwlk  33385  cvmlift3lem2  33581  cvmlift3lem4  33583  cvmlift3lem5  33584  cvmlift3lem6  33585  cvmlift3lem9  33588  elmrsubrn  33781  bccolsum  33997  bj-bary1lem  35637  finixpnum  35918  poimirlem4  35937  poimirlem16  35949  poimirlem19  35952  poimirlem25  35958  mblfinlem3  35972  dvtan  35983  itg2addnc  35987  itgaddnclem2  35992  ftc1anclem6  36011  areacirclem5  36025  areacirc  36026  upixp  36043  prdsbnd2  36109  ismrer1  36152  rngoneglmul  36257  rngoisocnv  36295  islshpsm  37298  lshpnel2N  37303  lfl0f  37387  ldualvsdi1  37461  ldualgrplem  37463  cmtcomlemN  37566  cvlsupr8  37667  pmodl42N  38170  pmapjat1  38172  llnmod2i2  38182  dalawlem2  38191  pmapj2N  38248  idltrn  38469  cdlemc6  38515  cdleme20d  38631  cdleme22e  38663  cdleme22eALTN  38664  cdleme35b  38769  cdleme48fvg  38819  cdlemg4d  38932  cdlemg8a  38946  cdlemg42  39048  cdlemg47a  39053  tendodi1  39103  tendodi2  39104  cdlemk4  39153  cdlemk21N  39192  cdlemk22  39212  cdlemky  39245  cdlemk53b  39275  cdlemk53  39276  cdlemkyyN  39281  erngdvlem3-rN  39317  tendocnv  39340  dia1dim2  39381  dicvaddcl  39509  dihglblem3N  39614  dihmeetlem4preN  39625  dihmeet2  39665  lcfl7lem  39818  baerlem3lem1  40026  baerlem5alem1  40027  mapdh6bN  40056  mapdh6cN  40057  mapdh6dN  40058  hdmap1l6b  40130  hdmap1l6c  40131  hdmap1l6d  40132  hdmap14lem13  40199  ofun  40514  mhphf  40596  nn0expgcd  40646  flt4lem7  40809  3cubeslem2  40820  3cubeslem3r  40822  3cubeslem4  40824  pellexlem2  40965  rmxyneg  41056  oddcomabszz  41080  acongeq  41119  hausgraph  41351  fsovrfovd  41990  inductionexd  42138  expgrowth  42326  binomcxplemwb  42339  binomcxplemnn0  42340  binomcxplemnotnn0  42347  sumsnd  42942  restuni4  43043  fmuldfeqlem1  43511  cncfmptss  43516  climexp  43534  dvresntr  43847  stoweidlem17  43946  wallispi  43999  dirkertrigeq  44030  dirkercncflem2  44033  fourierdlem30  44066  fourierdlem41  44077  fourierdlem81  44116  fourierdlem103  44138  sge0xp  44356  sge0isummpt2  44359  isomennd  44458  vonioolem1  44607  sigarperm  44779  fcores  44979  imasetpreimafvbijlemfo  45275  fundcmpsurbijinjpreimafv  45277  fundcmpsurinjimaid  45281  prprspr2  45388  opoeALTV  45553  c0mgm  45885  c0mhm  45886  zrrnghm  45893  cznrng  45931  rngchomrnghmresALTV  45972  fdmdifeqresdif  46095  lincsum  46188  lincscm  46189  lmod1lem4  46249  blennngt2o2  46356  blennn0e2  46358  topdlat  46708  reccot  46878  rectan  46879  cotsqcscsq  46882  amgmlemALT  46925