Theorem 3eqtrd 2268

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

Hypotheses

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

Assertion

Ref	Expression
3eqtrd	|- ( ph -> A = D )

Proof of Theorem 3eqtrd

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

Syntax hints:   -> wi 4   = wceq 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  tpeq123d  3763  diftpsn3  3814  oteq123d  3877  resiima  5094  fvun1  5712  fvmptd  5727  fmptpr  5846  caovlem2d  6215  offval  6243  ofvalg  6245  cnvf1olem  6389  nnm1  6693  updjudhcoinlf  7279  updjudhcoinrg  7280  caseinl  7290  caseinr  7291  omp1eomlem  7293  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  ltexnqq  7628  prarloclemarch  7638  ltrnqg  7640  nq02m  7685  prarloclemcalc  7722  mulnqprl  7788  mulnqpru  7789  ltexprlemloc  7827  addcanprleml  7834  recexprlem1ssu  7854  cauappcvgprlem1  7879  caucvgsrlemfv  8011  caucvgsrlemoffval  8016  recidpirqlemcalc  8077  axmulass  8093  axrnegex  8099  muladd11r  8335  addcan2  8360  addsub  8390  subsub2  8407  negsubdi2  8438  muladd  8563  mulsub  8580  cru  8782  mulreim  8784  recextlem1  8831  mulap0  8834  muleqadd  8848  divrecap  8868  div23ap  8871  div12ap  8874  divmulasscomap  8876  divcanap7  8901  conjmulap  8909  apmul1  8968  nndivtr  9185  subhalfhalf  9379  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  qapne  9873  xnegneg  10068  rexsub  10088  xnegid  10094  fseq1p1m1  10329  nn0split  10371  nnsplit  10372  fzosplitsnm1  10455  fzosplitpr  10480  fzosplitprm1  10481  ceilid  10578  flqdiv  10584  zmod10  10603  modqcyc  10622  modqaddabs  10625  mulqaddmodid  10627  modqadd2mod  10637  modqm1p1mod0  10638  modqmul12d  10641  modqadd12d  10643  modqmulmodr  10653  modqaddmulmod  10654  frecuzrdgsuc  10677  seqeq123d  10719  seqvalcd  10724  seq3f1olemqsumkj  10774  seq3f1oleml  10779  seqf1oglem2  10783  seq3id3  10787  seq3id  10788  seq3homo  10790  seq3z  10791  seqhomog  10793  exp1  10808  expnegap0  10810  expmulzap  10848  m1expeven  10849  expdivap  10853  binom3  10920  sqoddm1div8  10956  mulsubdivbinom2ap  10974  bcn1  11021  bcnp1n  11022  bcval5  11026  bcn2m1  11032  bcn2p1  11033  hashdifpr  11085  ccatlen  11176  ccatalpha  11194  ccatw2s1leng  11219  ccats1val2  11221  lswccats1  11224  swrdlend  11243  ccatswrd  11255  pfxmpt  11265  pfxfv  11269  pfxfvlsw  11280  ccatpfx  11286  pfx1  11288  pfxswrd  11291  swrdpfx  11292  pfxpfx  11293  lenrevpfxcctswrd  11297  wrdind  11307  wrd2ind  11308  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatpfx2  11322  pfxccatid  11326  cats1fvnd  11350  crim  11436  remullem  11449  remul2  11451  immul2  11458  ipcnval  11464  cjreim  11481  recvguniqlem  11572  resqrexlemover  11588  resqrexlemcalc1  11592  absid  11649  amgm2  11696  max0addsup  11797  minabs  11814  xrmaxrecl  11833  xrminadd  11853  fsumsplitf  11987  sumsnf  11988  fsump1i  12012  fsum2dlemstep  12013  fsumshftm  12024  fsummulc2  12027  modfsummodlemstep  12036  telfsumo  12045  fsumrelem  12050  hash2iun1dif1  12059  binomlem  12062  binom1dif  12066  arisum  12077  geo2sum  12093  geo2sum2  12094  cvgratz  12111  mertenslemi1  12114  clim2prod  12118  fprodeq0  12196  fprod2dlemstep  12201  fproddivap  12209  fproddivapf  12210  fprodmodd  12220  ef0lem  12239  eftlub  12269  efsep  12270  effsumlt  12271  tanval2ap  12292  efi4p  12296  resin4p  12297  recos4p  12298  efeul  12313  sinadd  12315  cosadd  12316  sinmul  12323  ef01bndlem  12335  cos12dec  12347  absef  12349  demoivreALT  12353  dvds2ln  12403  dvdseq  12427  opeo  12476  bezoutlemnewy  12585  nninfctlemfo  12629  eucalginv  12646  eucalglt  12647  eucalg  12649  lcmgcdlem  12667  lcm1  12671  divgcdcoprmex  12692  2sqpwodd  12766  zgcdsq  12791  qden1elz  12795  phiprmpw  12812  eulerthlem1  12817  eulerthlemrprm  12819  prmdiv  12825  hashgcdlem  12828  odzdvds  12836  vfermltl  12842  modprm0  12845  pythagtriplem12  12866  pcqmul  12894  pcaddlem  12930  pcadd  12931  pcadd2  12932  pcmpt  12934  pcmpt2  12935  mul4sqlem  12984  4sqlem11  12992  4sqlem17  12998  nninfdclemp1  13089  ressressg  13176  gsumsplit1r  13499  gsumprval  13500  mndinvmod  13546  mhmco  13591  gsumfzz  13596  grpinvid2  13654  grpasscan2  13665  grpinvssd  13678  grpinvadd  13679  grpsubid1  13686  grpsubadd  13689  grppncan  13692  mulg1  13734  mulgaddcomlem  13750  mulgdirlem  13758  mulgneg2  13761  mulgmodid  13766  nmzsubg  13815  qusinv  13841  qussub  13842  conjnmz  13884  ablsub2inv  13916  abladdsub4  13919  abladdsub  13920  ablpncan2  13921  ablpnpcan  13925  ablnncan  13926  invghm  13934  gsumfzconst  13946  gsumfzsnfd  13950  rngm2neg  13981  srgpcompp  14023  srgpcomppsc  14024  ringinvnzdiv  14082  ringm2neg  14087  dvr1  14171  dvrcan1  14173  dvrcan3  14174  rdivmuldivd  14177  lmodfopne  14359  sralemg  14471  gsumfzfsumlemm  14620  mplsubgfilemcl  14732  mplsubgfileminv  14733  xmetxpbl  15251  ivthinclemuopn  15381  limcimolemlt  15407  cnplimcim  15410  limccnpcntop  15418  limccnp2lem  15419  dvexp  15454  dvmptcmulcn  15464  dvply1  15508  ef2kpi  15549  sinhalfpip  15563  sinhalfpim  15564  coshalfpim  15566  ptolemy  15567  tangtx  15581  rpabscxpbnd  15683  relogbexpap  15701  rplogbcxp  15706  rpcxplogb  15707  binom4  15722  wilthlem1  15723  0sgm  15728  mpodvdsmulf1o  15733  fsumdvdsmul  15734  sgmppw  15735  0sgmppw  15736  1sgm2ppw  15738  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgsval2lem  15758  lgsval4  15768  lgsval4a  15770  lgsneg  15772  lgsneg1  15773  lgsdirprm  15782  lgsdir  15783  lgsne0  15786  lgsmulsqcoprm  15794  gausslemma2dlem1a  15806  gausslemma2dlem6  15815  gausslemma2d  15817  lgseisenlem3  15820  lgseisenlem4  15821  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem1  15829  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgslem3d1  15848  2sqlem3  15865  structiedg0val  15910  uhgr2edg  16076  usgr1e  16111  vtxdgfifival  16161  vtxdfifiun  16167  vtxdumgrfival  16168  vtxduspgrfvedgfi  16171  1loopgredg  16174  1loopgrvd2fi  16175  1hevtxdg1en  16178  p1evtxdeqfi  16182  edginwlkd  16225  clwwlknonex2lem1  16307  eupthvdres  16345  peano4nninf  16659  trilpolemclim  16691  trilpolemeq1  16695  apdifflemf  16701  gfsumval  16732  gfsumsn  16737