Theorem 3eqtr4rd 2655

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

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  csbun  3961  csbcnvgALT  5229  csbres  5320  fimacnvinrn2  6257  odi  7546  phplem4  8027  cantnfp1lem3  8460  cantnfp1  8461  cardidm  8668  ackbij2lem2  8945  ackbij2lem3  8946  divneg  10598  xadddilem  11996  xadddi2  11999  dfceil2  12502  modlt  12541  modmulnn  12550  seqcaopr3  12698  bcval5  12967  hashgadd  13027  hashun3  13034  seqcoll  13105  swrdccatwrd  13320  cshwmodn  13392  2cshwcom  13413  cshimadifsn0  13427  revco  13431  cshco  13433  ofccat  13556  relexpsucl  13621  cjreb  13711  recj  13712  imcj  13720  imval2  13739  sqrtmul  13848  absmax  13917  amgm2  13957  summolem2a  14293  fsumf1o  14301  sumsn  14319  sumsplit  14341  fsummulc2  14358  binom  14401  bcxmas  14406  incexclem  14407  incexc  14408  expcnv  14435  cvgrat  14454  prodmolem3  14502  prodmolem2a  14503  fprodf1o  14515  prodsn  14531  prodsnf  14533  fprodabs  14543  binomfallfac  14611  fallfacval4  14613  bcfallfac  14614  ege2le3  14659  efaddlem  14662  eftlub  14678  tanval3  14703  tanneg  14717  cosmul  14742  cos01bnd  14755  demoivreALT  14770  flodddiv4  14975  absmulgcd  15104  lcmfunsnlem2  15191  eulerthlem2  15325  phisum  15333  pythagtriplem14  15371  pcmul  15394  pcfac  15441  prmreclem6  15463  4sqlem12  15498  vdwlem6  15528  oppccatid  16202  curf2ndf  16710  oppcyon  16732  joincomALT  16852  meetcomALT  16854  pwsco1mhm  17193  sgrp2nmndlem4  17238  qusgrp2  17356  mulgnn0p1  17375  mulgneg  17383  mulgnn0dir  17394  qusghm  17520  gaid  17555  pmtrdifellem3  17721  psgnunilem2  17738  odmulg  17796  sylow1lem2  17837  sylow2a  17857  sylow3lem1  17865  efgredleme  17979  efgcpbllemb  17991  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  srgpcomp  18355  srgbinom  18368  lmodvsmmulgdi  18721  lmodsubdi  18743  0lmhm  18861  lspsneq  18943  qusrhm  19058  quscrng  19061  asclrhm  19163  resspsrmul  19238  evlsscasrng  19347  psropprmul  19429  evls1scasrng  19524  zringlpirlem3  19653  mulgrhm  19665  phssip  19822  frlmip  19936  frlmphl  19939  mat1ghm  20108  mat1mhm  20109  1marepvmarrepid  20200  mdetrlin  20227  mdetrsca2  20229  mdetunilem7  20243  mdetunilem9  20245  mndifsplit  20261  maducoeval2  20265  smadiadetglem2  20297  decpmatmul  20396  pm2mpghm  20440  pm2mpmhmlem2  20443  cpmidgsum2  20503  ptbasfi  21194  ptuni  21207  alexsubALTlem3  21663  subgtgp  21719  tsmsxplem1  21766  xmsusp  22184  restmetu  22185  nminv  22235  nrginvrcnlem  22305  copco  22626  pcoass  22632  pi1bas  22646  pi1xfrf  22661  pi1xfr  22663  isclmp  22705  cph2subdi  22818  cphassr  22820  tchcphlem1  22842  cphipval  22850  rrxip  22986  rrxnm  22987  pjthlem1  23016  ovolunlem1a  23071  ovolfs2  23145  uniiccdif  23152  ismbf  23203  itgaddlem2  23396  ditgswap  23429  ply1divex  23700  plyeq0lem  23770  plymullem1  23774  dgrcolem2  23834  vieta1lem2  23870  elqaalem2  23879  elqaalem3  23880  aaliou3lem7  23908  ulmshft  23948  mulcxplem  24230  cxpmul2  24235  root1eq1  24296  cxpeq  24298  logbchbase  24309  cosangneg2d  24337  isosctrlem2  24349  angpieqvdlem  24355  chordthmlem3  24361  chordthmlem4  24362  chordthmlem5  24363  quad2  24366  dcubic2  24371  cubic2  24375  quart1  24383  scvxcvx  24512  igamlgam  24576  lgam1  24590  basellem9  24615  ppifl  24686  mumul  24707  sgmmul  24726  chtublem  24736  chpub  24745  logfacrlim  24749  dchrsum2  24793  sumdchr2  24795  bposlem9  24817  lgsdir2  24855  lgsdir  24857  lgsdi  24859  lgsdirnn0  24869  lgsdinn0  24870  lgsquad3  24912  2sqblem  24956  chpo1ub  24969  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasum2if  24986  dchrisum0fmul  24995  rpvmasum2  25001  mulog2sumlem1  25023  vmalogdivsum2  25027  log2sumbnd  25033  selberg3lem1  25046  selberg4lem1  25049  pntrsumo1  25054  selbergr  25057  pntpbnd1  25075  pntlemk  25095  tgbtwnconn1lem3  25269  mideulem2  25426  axlowdimlem16  25637  axcontlem8  25651  clwlkfoclwwlk  26372  ex-ind-dvds  26710  vsfval  26872  lnocoi  26996  nmblolbii  27038  ipasslem5  27074  hvsubid  27267  sshjval3  27597  pjhthlem1  27634  adjval  28133  unopf1o  28159  kbpj  28199  lnopmi  28243  nmcoplbi  28271  cnlnadjlem2  28311  adjadd  28336  branmfn  28348  pjtoi  28422  ofoprabco  28847  xrsmulgzz  29009  archiabllem1a  29076  gsumvsca1  29113  gsumvsca2  29114  rdivmuldivd  29122  psgnfzto1stlem  29181  submat1n  29199  submatres  29200  madjusmdetlem3  29223  xrge0iifhom  29311  qqhval2lem  29353  qqhrhm  29361  qqhucn  29364  esumsnf  29453  measvunilem0  29603  carsgclctunlem1  29706  ballotlemfp1  29880  ballotlemsf1o  29902  signstfveq0  29980  cvmlift3lem2  30556  cvmlift3lem4  30558  cvmlift3lem5  30559  cvmlift3lem6  30560  cvmlift3lem9  30563  elmrsubrn  30671  bccolsum  30878  bj-bary1lem  32337  csbdif  32347  finixpnum  32564  poimirlem4  32583  poimirlem16  32595  poimirlem19  32598  poimirlem25  32604  mblfinlem3  32618  dvtan  32630  itg2addnc  32634  itgaddnclem2  32639  ftc1anclem6  32660  areacirclem5  32674  areacirc  32675  upixp  32694  prdsbnd2  32764  ismrer1  32807  rngoneglmul  32912  rngoisocnv  32950  islshpsm  33285  lshpnel2N  33290  lfl0f  33374  ldualvsdi1  33448  ldualgrplem  33450  cmtcomlemN  33553  cvlsupr8  33654  pmodl42N  34155  pmapjat1  34157  llnmod2i2  34167  dalawlem2  34176  pmapj2N  34233  idltrn  34454  cdlemc6  34501  cdleme20d  34618  cdleme22e  34650  cdleme22eALTN  34651  cdleme35b  34756  cdleme48fvg  34806  cdlemg4d  34919  cdlemg8a  34933  cdlemg42  35035  cdlemg47a  35040  tendodi1  35090  tendodi2  35091  cdlemk4  35140  cdlemk21N  35179  cdlemk22  35199  cdlemky  35232  cdlemk53b  35262  cdlemk53  35263  cdlemkyyN  35268  erngdvlem3-rN  35304  tendocnv  35328  dia1dim2  35369  dicvaddcl  35497  dihglblem3N  35602  dihmeetlem4preN  35613  dihmeet2  35653  lcfl7lem  35806  baerlem3lem1  36014  baerlem5alem1  36015  mapdh6bN  36044  mapdh6cN  36045  mapdh6dN  36046  hdmap1l6b  36119  hdmap1l6c  36120  hdmap1l6d  36121  hdmap14lem13  36190  pellexlem2  36412  rmxyneg  36503  oddcomabszz  36527  acongeq  36568  hausgraph  36809  fsovrfovd  37323  inductionexd  37473  expgrowth  37556  binomcxplemwb  37569  binomcxplemnn0  37570  binomcxplemnotnn0  37577  sumsnd  38208  restuni4  38336  sumsnf  38636  fmuldfeqlem1  38649  cncfmptss  38654  climexp  38672  dvresntr  38806  stoweidlem17  38910  wallispi  38963  dirkertrigeq  38994  dirkercncflem2  38997  fourierdlem30  39030  fourierdlem41  39041  fourierdlem81  39080  fourierdlem103  39102  sge0xp  39322  sge0isummpt2  39325  isomennd  39421  vonioolem1  39571  sigarperm  39698  pwdif  40039  opoeALTV  40132  clwlksfoclwwlk  41270  lp1cycl  41319  c0mgm  41699  c0mhm  41700  zrrnghm  41707  cznrng  41747  rngchomrnghmresALTV  41788  fdmdifeqresdif  41913  lincsum  42012  lincscm  42013  lmod1lem4  42073  blennngt2o2  42184  blennn0e2  42186  reccot  42298  rectan  42299  cotsqcscsq  42302  amgmlemALT  42358