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  5700  fvmptd  5715  fmptpr  5831  caovlem2d  6198  offval  6226  ofvalg  6228  cnvf1olem  6370  nnm1  6671  updjudhcoinlf  7247  updjudhcoinrg  7248  caseinl  7258  caseinr  7259  omp1eomlem  7261  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  ltexnqq  7595  prarloclemarch  7605  ltrnqg  7607  nq02m  7652  prarloclemcalc  7689  mulnqprl  7755  mulnqpru  7756  ltexprlemloc  7794  addcanprleml  7801  recexprlem1ssu  7821  cauappcvgprlem1  7846  caucvgsrlemfv  7978  caucvgsrlemoffval  7983  recidpirqlemcalc  8044  axmulass  8060  axrnegex  8066  muladd11r  8302  addcan2  8327  addsub  8357  subsub2  8374  negsubdi2  8405  muladd  8530  mulsub  8547  cru  8749  mulreim  8751  recextlem1  8798  mulap0  8801  muleqadd  8815  divrecap  8835  div23ap  8838  div12ap  8841  divmulasscomap  8843  divcanap7  8868  conjmulap  8876  apmul1  8935  nndivtr  9152  subhalfhalf  9346  xp1d2m1eqxm1d2  9364  div4p1lem1div2  9365  qapne  9834  xnegneg  10029  rexsub  10049  xnegid  10055  fseq1p1m1  10290  nn0split  10332  nnsplit  10333  fzosplitsnm1  10415  fzosplitprm1  10440  ceilid  10537  flqdiv  10543  zmod10  10562  modqcyc  10581  modqaddabs  10584  mulqaddmodid  10586  modqadd2mod  10596  modqm1p1mod0  10597  modqmul12d  10600  modqadd12d  10602  modqmulmodr  10612  modqaddmulmod  10613  frecuzrdgsuc  10636  seqeq123d  10678  seqvalcd  10683  seq3f1olemqsumkj  10733  seq3f1oleml  10738  seqf1oglem2  10742  seq3id3  10746  seq3id  10747  seq3homo  10749  seq3z  10750  seqhomog  10752  exp1  10767  expnegap0  10769  expmulzap  10807  m1expeven  10808  expdivap  10812  binom3  10879  sqoddm1div8  10915  mulsubdivbinom2ap  10933  bcn1  10980  bcnp1n  10981  bcval5  10985  bcn2m1  10991  bcn2p1  10992  hashdifpr  11042  ccatlen  11130  ccats1val2  11171  lswccats1  11174  swrdlend  11190  ccatswrd  11202  pfxmpt  11212  pfxfv  11216  pfxfvlsw  11227  ccatpfx  11233  pfx1  11235  pfxswrd  11238  swrdpfx  11239  pfxpfx  11240  lenrevpfxcctswrd  11244  wrdind  11254  wrd2ind  11255  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatpfx2  11269  pfxccatid  11273  cats1fvnd  11297  crim  11369  remullem  11382  remul2  11384  immul2  11391  ipcnval  11397  cjreim  11414  recvguniqlem  11505  resqrexlemover  11521  resqrexlemcalc1  11525  absid  11582  amgm2  11629  max0addsup  11730  minabs  11747  xrmaxrecl  11766  xrminadd  11786  fsumsplitf  11919  sumsnf  11920  fsump1i  11944  fsum2dlemstep  11945  fsumshftm  11956  fsummulc2  11959  modfsummodlemstep  11968  telfsumo  11977  fsumrelem  11982  hash2iun1dif1  11991  binomlem  11994  binom1dif  11998  arisum  12009  geo2sum  12025  geo2sum2  12026  cvgratz  12043  mertenslemi1  12046  clim2prod  12050  fprodeq0  12128  fprod2dlemstep  12133  fproddivap  12141  fproddivapf  12142  fprodmodd  12152  ef0lem  12171  eftlub  12201  efsep  12202  effsumlt  12203  tanval2ap  12224  efi4p  12228  resin4p  12229  recos4p  12230  efeul  12245  sinadd  12247  cosadd  12248  sinmul  12255  ef01bndlem  12267  cos12dec  12279  absef  12281  demoivreALT  12285  dvds2ln  12335  dvdseq  12359  opeo  12408  bezoutlemnewy  12517  nninfctlemfo  12561  eucalginv  12578  eucalglt  12579  eucalg  12581  lcmgcdlem  12599  lcm1  12603  divgcdcoprmex  12624  2sqpwodd  12698  zgcdsq  12723  qden1elz  12727  phiprmpw  12744  eulerthlem1  12749  eulerthlemrprm  12751  prmdiv  12757  hashgcdlem  12760  odzdvds  12768  vfermltl  12774  modprm0  12777  pythagtriplem12  12798  pcqmul  12826  pcaddlem  12862  pcadd  12863  pcadd2  12864  pcmpt  12866  pcmpt2  12867  mul4sqlem  12916  4sqlem11  12924  4sqlem17  12930  nninfdclemp1  13021  ressressg  13108  gsumsplit1r  13431  gsumprval  13432  mndinvmod  13478  mhmco  13523  gsumfzz  13528  grpinvid2  13586  grpasscan2  13597  grpinvssd  13610  grpinvadd  13611  grpsubid1  13618  grpsubadd  13621  grppncan  13624  mulg1  13666  mulgaddcomlem  13682  mulgdirlem  13690  mulgneg2  13693  mulgmodid  13698  nmzsubg  13747  qusinv  13773  qussub  13774  conjnmz  13816  ablsub2inv  13848  abladdsub4  13851  abladdsub  13852  ablpncan2  13853  ablpnpcan  13857  ablnncan  13858  invghm  13866  gsumfzconst  13878  gsumfzsnfd  13882  rngm2neg  13912  srgpcompp  13954  srgpcomppsc  13955  ringinvnzdiv  14013  ringm2neg  14018  dvr1  14102  dvrcan1  14104  dvrcan3  14105  rdivmuldivd  14108  lmodfopne  14290  sralemg  14402  gsumfzfsumlemm  14551  mplsubgfilemcl  14663  mplsubgfileminv  14664  xmetxpbl  15182  ivthinclemuopn  15312  limcimolemlt  15338  cnplimcim  15341  limccnpcntop  15349  limccnp2lem  15350  dvexp  15385  dvmptcmulcn  15395  dvply1  15439  ef2kpi  15480  sinhalfpip  15494  sinhalfpim  15495  coshalfpim  15497  ptolemy  15498  tangtx  15512  rpabscxpbnd  15614  relogbexpap  15632  rplogbcxp  15637  rpcxplogb  15638  binom4  15653  wilthlem1  15654  0sgm  15659  mpodvdsmulf1o  15664  fsumdvdsmul  15665  sgmppw  15666  0sgmppw  15667  1sgm2ppw  15669  perfectlem1  15673  perfectlem2  15674  perfect  15675  lgsval2lem  15689  lgsval4  15699  lgsval4a  15701  lgsneg  15703  lgsneg1  15704  lgsdirprm  15713  lgsdir  15714  lgsne0  15717  lgsmulsqcoprm  15725  gausslemma2dlem1a  15737  gausslemma2dlem6  15746  gausslemma2d  15748  lgseisenlem3  15751  lgseisenlem4  15752  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem1  15760  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgslem3d1  15779  2sqlem3  15796  structiedg0val  15841  uhgr2edg  16004  edginwlkd  16066  peano4nninf  16372  trilpolemclim  16404  trilpolemeq1  16408  apdifflemf  16414