Theorem 3eqtrd 2266

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 2262	. 2 |- ( ph -> B = D )
5	1, 4	eqtrd 2262	1 |- ( ph -> A = D )

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  tpeq123d  3758  diftpsn3  3809  oteq123d  3872  resiima  5086  fvun1  5702  fvmptd  5717  fmptpr  5835  caovlem2d  6204  offval  6232  ofvalg  6234  cnvf1olem  6376  nnm1  6679  updjudhcoinlf  7258  updjudhcoinrg  7259  caseinl  7269  caseinr  7270  omp1eomlem  7272  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  ltexnqq  7606  prarloclemarch  7616  ltrnqg  7618  nq02m  7663  prarloclemcalc  7700  mulnqprl  7766  mulnqpru  7767  ltexprlemloc  7805  addcanprleml  7812  recexprlem1ssu  7832  cauappcvgprlem1  7857  caucvgsrlemfv  7989  caucvgsrlemoffval  7994  recidpirqlemcalc  8055  axmulass  8071  axrnegex  8077  muladd11r  8313  addcan2  8338  addsub  8368  subsub2  8385  negsubdi2  8416  muladd  8541  mulsub  8558  cru  8760  mulreim  8762  recextlem1  8809  mulap0  8812  muleqadd  8826  divrecap  8846  div23ap  8849  div12ap  8852  divmulasscomap  8854  divcanap7  8879  conjmulap  8887  apmul1  8946  nndivtr  9163  subhalfhalf  9357  xp1d2m1eqxm1d2  9375  div4p1lem1div2  9376  qapne  9846  xnegneg  10041  rexsub  10061  xnegid  10067  fseq1p1m1  10302  nn0split  10344  nnsplit  10345  fzosplitsnm1  10427  fzosplitprm1  10452  ceilid  10549  flqdiv  10555  zmod10  10574  modqcyc  10593  modqaddabs  10596  mulqaddmodid  10598  modqadd2mod  10608  modqm1p1mod0  10609  modqmul12d  10612  modqadd12d  10614  modqmulmodr  10624  modqaddmulmod  10625  frecuzrdgsuc  10648  seqeq123d  10690  seqvalcd  10695  seq3f1olemqsumkj  10745  seq3f1oleml  10750  seqf1oglem2  10754  seq3id3  10758  seq3id  10759  seq3homo  10761  seq3z  10762  seqhomog  10764  exp1  10779  expnegap0  10781  expmulzap  10819  m1expeven  10820  expdivap  10824  binom3  10891  sqoddm1div8  10927  mulsubdivbinom2ap  10945  bcn1  10992  bcnp1n  10993  bcval5  10997  bcn2m1  11003  bcn2p1  11004  hashdifpr  11055  ccatlen  11143  ccatalpha  11161  ccats1val2  11187  lswccats1  11190  swrdlend  11206  ccatswrd  11218  pfxmpt  11228  pfxfv  11232  pfxfvlsw  11243  ccatpfx  11249  pfx1  11251  pfxswrd  11254  swrdpfx  11255  pfxpfx  11256  lenrevpfxcctswrd  11260  wrdind  11270  wrd2ind  11271  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatpfx2  11285  pfxccatid  11289  cats1fvnd  11313  crim  11385  remullem  11398  remul2  11400  immul2  11407  ipcnval  11413  cjreim  11430  recvguniqlem  11521  resqrexlemover  11537  resqrexlemcalc1  11541  absid  11598  amgm2  11645  max0addsup  11746  minabs  11763  xrmaxrecl  11782  xrminadd  11802  fsumsplitf  11935  sumsnf  11936  fsump1i  11960  fsum2dlemstep  11961  fsumshftm  11972  fsummulc2  11975  modfsummodlemstep  11984  telfsumo  11993  fsumrelem  11998  hash2iun1dif1  12007  binomlem  12010  binom1dif  12014  arisum  12025  geo2sum  12041  geo2sum2  12042  cvgratz  12059  mertenslemi1  12062  clim2prod  12066  fprodeq0  12144  fprod2dlemstep  12149  fproddivap  12157  fproddivapf  12158  fprodmodd  12168  ef0lem  12187  eftlub  12217  efsep  12218  effsumlt  12219  tanval2ap  12240  efi4p  12244  resin4p  12245  recos4p  12246  efeul  12261  sinadd  12263  cosadd  12264  sinmul  12271  ef01bndlem  12283  cos12dec  12295  absef  12297  demoivreALT  12301  dvds2ln  12351  dvdseq  12375  opeo  12424  bezoutlemnewy  12533  nninfctlemfo  12577  eucalginv  12594  eucalglt  12595  eucalg  12597  lcmgcdlem  12615  lcm1  12619  divgcdcoprmex  12640  2sqpwodd  12714  zgcdsq  12739  qden1elz  12743  phiprmpw  12760  eulerthlem1  12765  eulerthlemrprm  12767  prmdiv  12773  hashgcdlem  12776  odzdvds  12784  vfermltl  12790  modprm0  12793  pythagtriplem12  12814  pcqmul  12842  pcaddlem  12878  pcadd  12879  pcadd2  12880  pcmpt  12882  pcmpt2  12883  mul4sqlem  12932  4sqlem11  12940  4sqlem17  12946  nninfdclemp1  13037  ressressg  13124  gsumsplit1r  13447  gsumprval  13448  mndinvmod  13494  mhmco  13539  gsumfzz  13544  grpinvid2  13602  grpasscan2  13613  grpinvssd  13626  grpinvadd  13627  grpsubid1  13634  grpsubadd  13637  grppncan  13640  mulg1  13682  mulgaddcomlem  13698  mulgdirlem  13706  mulgneg2  13709  mulgmodid  13714  nmzsubg  13763  qusinv  13789  qussub  13790  conjnmz  13832  ablsub2inv  13864  abladdsub4  13867  abladdsub  13868  ablpncan2  13869  ablpnpcan  13873  ablnncan  13874  invghm  13882  gsumfzconst  13894  gsumfzsnfd  13898  rngm2neg  13928  srgpcompp  13970  srgpcomppsc  13971  ringinvnzdiv  14029  ringm2neg  14034  dvr1  14118  dvrcan1  14120  dvrcan3  14121  rdivmuldivd  14124  lmodfopne  14306  sralemg  14418  gsumfzfsumlemm  14567  mplsubgfilemcl  14679  mplsubgfileminv  14680  xmetxpbl  15198  ivthinclemuopn  15328  limcimolemlt  15354  cnplimcim  15357  limccnpcntop  15365  limccnp2lem  15366  dvexp  15401  dvmptcmulcn  15411  dvply1  15455  ef2kpi  15496  sinhalfpip  15510  sinhalfpim  15511  coshalfpim  15513  ptolemy  15514  tangtx  15528  rpabscxpbnd  15630  relogbexpap  15648  rplogbcxp  15653  rpcxplogb  15654  binom4  15669  wilthlem1  15670  0sgm  15675  mpodvdsmulf1o  15680  fsumdvdsmul  15681  sgmppw  15682  0sgmppw  15683  1sgm2ppw  15685  perfectlem1  15689  perfectlem2  15690  perfect  15691  lgsval2lem  15705  lgsval4  15715  lgsval4a  15717  lgsneg  15719  lgsneg1  15720  lgsdirprm  15729  lgsdir  15730  lgsne0  15733  lgsmulsqcoprm  15741  gausslemma2dlem1a  15753  gausslemma2dlem6  15762  gausslemma2d  15764  lgseisenlem3  15767  lgseisenlem4  15768  lgseisen  15769  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem1  15776  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2lgslem3d1  15795  2sqlem3  15812  structiedg0val  15857  uhgr2edg  16020  vtxdgfifival  16051  vtxdfifiun  16057  vtxdumgrfival  16058  vtxduspgrfvedgfi  16061  edginwlkd  16101  peano4nninf  16460  trilpolemclim  16492  trilpolemeq1  16496  apdifflemf  16502