Theorem 3eqtr4rd 2667

Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)

Hypotheses

Ref	Expression
3eqtr4d.1	|- ( ph -> A = B )
3eqtr4d.2	|- ( ph -> C = A )
3eqtr4d.3	|- ( ph -> D = B )

Assertion

Ref	Expression
3eqtr4rd	|- ( ph -> D = C )

Proof of Theorem 3eqtr4rd

Step	Hyp	Ref	Expression
1		3eqtr4d.3	. . 3 |- ( ph -> D = B )
2		3eqtr4d.1	. . 3 |- ( ph -> A = B )
3	1, 2	eqtr4d 2659	. 2 |- ( ph -> D = A )
4		3eqtr4d.2	. 2 |- ( ph -> C = A )
5	3, 4	eqtr4d 2659	1 |- ( ph -> D = C )

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  csbun  4009  csbcnvgALT  5307  csbres  5399  fimacnvinrn2  6349  odi  7659  phplem4  8142  cantnfp1lem3  8577  cantnfp1  8578  cardidm  8785  ackbij2lem2  9062  ackbij2lem3  9063  divneg  10719  xadddilem  12124  xadddi2  12127  dfceil2  12640  modlt  12679  modmulnn  12688  seqcaopr3  12836  bcval5  13105  hashgadd  13166  hashun3  13173  seqcoll  13248  swrdccatwrd  13468  cshwmodn  13541  2cshwcom  13562  cshimadifsn0  13576  revco  13580  cshco  13582  ofccat  13708  relexpsucl  13773  cjreb  13863  recj  13864  imcj  13872  imval2  13891  sqrtmul  14000  absmax  14069  amgm2  14109  summolem2a  14446  fsumf1o  14454  sumsnf  14473  sumsn  14475  sumsplit  14499  fsummulc2  14516  binom  14562  bcxmas  14567  incexclem  14568  incexc  14569  expcnv  14596  cvgrat  14615  prodmolem3  14663  prodmolem2a  14664  fprodf1o  14676  prodsn  14692  prodsnf  14694  fprodabs  14704  binomfallfac  14772  fallfacval4  14774  bcfallfac  14775  ege2le3  14820  efaddlem  14823  eftlub  14839  tanval3  14864  tanneg  14878  cosmul  14903  cos01bnd  14916  demoivreALT  14931  flodddiv4  15137  absmulgcd  15266  lcmfunsnlem2  15353  eulerthlem2  15487  phisum  15495  pythagtriplem14  15533  pcmul  15556  pcfac  15603  prmreclem6  15625  4sqlem12  15660  vdwlem6  15690  oppccatid  16379  curf2ndf  16887  oppcyon  16909  joincomALT  17029  meetcomALT  17031  pwsco1mhm  17370  sgrp2nmndlem4  17415  qusgrp2  17533  mulgnn0p1  17552  mulgneg  17560  mulgnn0dir  17571  qusghm  17697  gaid  17732  pmtrdifellem3  17898  psgnunilem2  17915  odmulg  17973  sylow1lem2  18014  sylow2a  18034  sylow3lem1  18042  efgredleme  18156  efgcpbllemb  18168  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  srgpcomp  18532  srgbinom  18545  lmodvsmmulgdi  18898  lmodsubdi  18920  rmodislmodlem  18930  0lmhm  19040  lspsneq  19122  qusrhm  19237  quscrng  19240  asclrhm  19342  resspsrmul  19417  evlsscasrng  19526  psropprmul  19608  evls1scasrng  19703  zringlpirlem3  19834  mulgrhm  19846  phssip  20003  frlmip  20117  frlmphl  20120  mat1ghm  20289  mat1mhm  20290  1marepvmarrepid  20381  mdetrlin  20408  mdetrsca2  20410  mdetunilem7  20424  mdetunilem9  20426  mndifsplit  20442  maducoeval2  20446  smadiadetglem2  20478  decpmatmul  20577  pm2mpghm  20621  pm2mpmhmlem2  20624  cpmidgsum2  20684  ptbasfi  21384  ptuni  21397  alexsubALTlem3  21853  subgtgp  21909  tsmsxplem1  21956  xmsusp  22374  restmetu  22375  nminv  22425  nrginvrcnlem  22495  copco  22818  pcoass  22824  pi1bas  22838  pi1xfrf  22853  pi1xfr  22855  isclmp  22897  cph2subdi  23010  cphassr  23012  tchcphlem1  23034  cphipval  23042  rrxip  23178  rrxnm  23179  pjthlem1  23208  ovolunlem1a  23264  ovolfs2  23339  uniiccdif  23346  ismbf  23397  itgaddlem2  23590  ditgswap  23623  ply1divex  23896  plyeq0lem  23966  plymullem1  23970  dgrcolem2  24030  vieta1lem2  24066  elqaalem2  24075  elqaalem3  24076  aaliou3lem7  24104  ulmshft  24144  mulcxplem  24430  cxpmul2  24435  root1eq1  24496  cxpeq  24498  logbchbase  24509  cosangneg2d  24537  isosctrlem2  24549  angpieqvdlem  24555  chordthmlem3  24561  chordthmlem4  24562  chordthmlem5  24563  quad2  24566  dcubic2  24571  cubic2  24575  quart1  24583  scvxcvx  24712  igamlgam  24776  lgam1  24790  basellem9  24815  ppifl  24886  mumul  24907  sgmmul  24926  chtublem  24936  chpub  24945  logfacrlim  24949  dchrsum2  24993  sumdchr2  24995  bposlem9  25017  lgsdir2  25055  lgsdir  25057  lgsdi  25059  lgsdirnn0  25069  lgsdinn0  25070  lgsquad3  25112  2sqblem  25156  chpo1ub  25169  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2if  25186  dchrisum0fmul  25195  rpvmasum2  25201  mulog2sumlem1  25223  vmalogdivsum2  25227  log2sumbnd  25233  selberg3lem1  25246  selberg4lem1  25249  pntrsumo1  25254  selbergr  25257  pntpbnd1  25275  pntlemk  25295  tgbtwnconn1lem3  25469  mideulem2  25626  axlowdimlem16  25837  axcontlem8  25851  vtxval  25878  iedgval  25879  edgval  25941  vtxdgop  26366  finsumvtxdg2size  26446  clwlksfoclwwlk  26963  lp1cycl  27012  ex-ind-dvds  27318  vsfval  27488  lnocoi  27612  nmblolbii  27654  ipasslem5  27690  hvsubid  27883  sshjval3  28213  pjhthlem1  28250  adjval  28749  unopf1o  28775  kbpj  28815  lnopmi  28859  nmcoplbi  28887  cnlnadjlem2  28927  adjadd  28952  branmfn  28964  pjtoi  29038  ofoprabco  29464  xrsmulgzz  29678  archiabllem1a  29745  gsumvsca1  29782  gsumvsca2  29783  rdivmuldivd  29791  psgnfzto1stlem  29850  submat1n  29871  submatres  29872  madjusmdetlem3  29895  xrge0iifhom  29983  qqhval2lem  30025  qqhrhm  30033  qqhucn  30036  esumsnf  30126  measvunilem0  30276  carsgclctunlem1  30379  ballotlemfp1  30553  ballotlemsf1o  30575  signstfveq0  30654  breprexplemc  30710  breprexp  30711  breprexpnat  30712  circlemeth  30718  logdivsqrle  30728  hgt750lema  30735  cvmlift3lem2  31302  cvmlift3lem4  31304  cvmlift3lem5  31305  cvmlift3lem6  31306  cvmlift3lem9  31309  elmrsubrn  31417  bccolsum  31625  bj-bary1lem  33160  csbdif  33171  finixpnum  33394  poimirlem4  33413  poimirlem16  33425  poimirlem19  33428  poimirlem25  33434  mblfinlem3  33448  dvtan  33460  itg2addnc  33464  itgaddnclem2  33469  ftc1anclem6  33490  areacirclem5  33504  areacirc  33505  upixp  33524  prdsbnd2  33594  ismrer1  33637  rngoneglmul  33742  rngoisocnv  33780  islshpsm  34267  lshpnel2N  34272  lfl0f  34356  ldualvsdi1  34430  ldualgrplem  34432  cmtcomlemN  34535  cvlsupr8  34636  pmodl42N  35137  pmapjat1  35139  llnmod2i2  35149  dalawlem2  35158  pmapj2N  35215  idltrn  35436  cdlemc6  35483  cdleme20d  35600  cdleme22e  35632  cdleme22eALTN  35633  cdleme35b  35738  cdleme48fvg  35788  cdlemg4d  35901  cdlemg8a  35915  cdlemg42  36017  cdlemg47a  36022  tendodi1  36072  tendodi2  36073  cdlemk4  36122  cdlemk21N  36161  cdlemk22  36181  cdlemky  36214  cdlemk53b  36244  cdlemk53  36245  cdlemkyyN  36250  erngdvlem3-rN  36286  tendocnv  36310  dia1dim2  36351  dicvaddcl  36479  dihglblem3N  36584  dihmeetlem4preN  36595  dihmeet2  36635  lcfl7lem  36788  baerlem3lem1  36996  baerlem5alem1  36997  mapdh6bN  37026  mapdh6cN  37027  mapdh6dN  37028  hdmap1l6b  37101  hdmap1l6c  37102  hdmap1l6d  37103  hdmap14lem13  37172  pellexlem2  37394  rmxyneg  37485  oddcomabszz  37509  acongeq  37550  hausgraph  37790  fsovrfovd  38303  inductionexd  38453  expgrowth  38534  binomcxplemwb  38547  binomcxplemnn0  38548  binomcxplemnotnn0  38555  sumsnd  39185  restuni4  39304  fmuldfeqlem1  39814  cncfmptss  39819  climexp  39837  dvresntr  40132  stoweidlem17  40234  wallispi  40287  dirkertrigeq  40318  dirkercncflem2  40321  fourierdlem30  40354  fourierdlem41  40365  fourierdlem81  40404  fourierdlem103  40426  sge0xp  40646  sge0isummpt2  40649  isomennd  40745  vonioolem1  40894  sigarperm  41049  pwdif  41501  opoeALTV  41594  c0mgm  41909  c0mhm  41910  zrrnghm  41917  cznrng  41955  rngchomrnghmresALTV  41996  fdmdifeqresdif  42120  lincsum  42218  lincscm  42219  lmod1lem4  42279  blennngt2o2  42386  blennn0e2  42388  reccot  42499  rectan  42500  cotsqcscsq  42503  amgmlemALT  42549