Theorem 3eqtr4g 2287

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 |- C = A
2		3eqtr4g.1	. . 3 |- ( ph -> A = B )
3	1, 2	eqtrid 2274	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	eqtr4di 2280	1 |- ( ph -> C = 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:  rabbidva2  2786  rabeqf  2789  csbeq1  3127  csbeq2  3148  csbeq2d  3149  csbnestgf  3177  difeq1  3315  difeq2  3316  uneq2  3352  ineq2  3399  dfrab3ss  3482  ifeq1  3605  ifeq2  3606  ifbi  3623  pweq  3652  sneq  3677  csbsng  3727  rabsn  3733  preq1  3743  preq2  3744  tpeq1  3752  tpeq2  3753  tpeq3  3754  prprc1  3774  opeq1  3856  opeq2  3857  oteq1  3865  oteq2  3866  oteq3  3867  csbunig  3895  unieq  3896  inteq  3925  iineq1  3978  iineq2  3981  dfiin2g  3997  iinrabm  4027  iinin1m  4034  iinxprg  4039  opabbid  4148  mpteq12f  4163  suceq  4492  xpeq1  4732  xpeq2  4733  csbxpg  4799  csbdmg  4916  rneq  4950  reseq1  4998  reseq2  4999  csbresg  5007  resindm  5046  resmpt  5052  resmptf  5054  imaeq1  5062  imaeq2  5063  mptcnv  5130  csbrng  5189  dmpropg  5200  rnpropg  5207  cores  5231  cores2  5240  xpcom  5274  iotaeq  5286  iotabi  5287  fntpg  5376  funimaexg  5404  fveq1  5625  fveq2  5626  fvres  5650  csbfv12g  5666  fnimapr  5693  fndmin  5741  fprg  5821  fsnunfv  5839  fsnunres  5840  fliftf  5922  isoini2  5942  riotaeqdv  5954  riotabidv  5955  riotauni  5960  riotabidva  5971  snriota  5985  oveq  6006  oveq1  6007  oveq2  6008  oprabbid  6056  mpoeq123  6062  mpoeq123dva  6064  mpoeq3dva  6067  resmpo  6101  ovres  6144  f1ocnvd  6206  ofeqd  6218  ofeq  6219  ofreq  6220  f1od2  6379  ovtposg  6403  recseq  6450  tfr2a  6465  rdgeq1  6515  rdgeq2  6516  freceq1  6536  freceq2  6537  eceq1  6713  eceq2  6715  qseq1  6728  qseq2  6729  uniqs  6738  ecinxp  6755  qsinxp  6756  erovlem  6772  ixpeq1  6854  supeq1  7149  supeq2  7152  supeq3  7153  supeq123d  7154  infeq1  7174  infeq2  7177  infeq3  7178  infeq123d  7179  infisoti  7195  djueq12  7202  acneq  7380  addpiord  7499  mulpiord  7500  00sr  7952  negeq  8335  csbnegg  8340  negsubdi  8398  mulneg1  8537  deceq1  9578  deceq2  9579  xnegeq  10019  fseq1p1m1  10286  frec2uzsucd  10618  frec2uzrdg  10626  frecuzrdgsuc  10631  frecuzrdgg  10633  frecuzrdgsuctlem  10640  seqeq1  10667  seqeq2  10668  seqeq3  10669  seqvalcd  10678  seq3f1olemp  10732  hashprg  11025  s1eq  11147  s1prc  11151  s2eqd  11297  s3eqd  11298  s4eqd  11299  s5eqd  11300  s6eqd  11301  s7eqd  11302  s8eqd  11303  shftdm  11328  resqrexlemfp1  11515  negfi  11734  sumeq1  11861  sumeq2  11865  zsumdc  11890  isumss2  11899  fsumsplitsnun  11925  isumclim3  11929  fisumcom2  11944  isumshft  11996  prodeq1f  12058  prodeq2w  12062  prodeq2  12063  zproddc  12085  fprodm1s  12107  fprodp1s  12108  fprodcom2fi  12132  fprodsplitf  12138  ege2le3  12177  efgt1p2  12201  dfphi2  12737  prmdiveq  12753  pceulem  12812  sloteq  13032  setsslid  13078  ressval2  13094  ecqusaddd  13770  ringidvalg  13919  zrhpropd  14584  metreslem  15048  comet  15167  cnmetdval  15197  dvmptfsum  15393  dvply1  15433  lgsdi  15710  lgseisenlem2  15744  lgsquadlem3  15752  uhgrvtxedgiedgb  15935  usgredg2v  16016  redcwlpolemeq1  16381