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  3775  opeq1  3857  opeq2  3858  oteq1  3866  oteq2  3867  oteq3  3868  csbunig  3896  unieq  3897  inteq  3926  iineq1  3979  iineq2  3982  dfiin2g  3998  iinrabm  4028  iinin1m  4035  iinxprg  4040  opabbid  4149  mpteq12f  4164  suceq  4493  xpeq1  4733  xpeq2  4734  csbxpg  4800  csbdmg  4917  rneq  4951  reseq1  4999  reseq2  5000  csbresg  5008  resindm  5047  resmpt  5053  resmptf  5055  imaeq1  5063  imaeq2  5064  mptcnv  5131  csbrng  5190  dmpropg  5201  rnpropg  5208  cores  5232  cores2  5241  xpcom  5275  iotaeq  5287  iotabi  5288  fntpg  5377  funimaexg  5405  fveq1  5626  fveq2  5627  fvres  5651  csbfv12g  5667  fnimapr  5694  fndmin  5742  fprg  5822  fsnunfv  5840  fsnunres  5841  fliftf  5923  isoini2  5943  riotaeqdv  5955  riotabidv  5956  riotauni  5961  riotabidva  5972  snriota  5986  oveq  6007  oveq1  6008  oveq2  6009  oprabbid  6057  mpoeq123  6063  mpoeq123dva  6065  mpoeq3dva  6068  resmpo  6102  ovres  6145  f1ocnvd  6208  ofeqd  6220  ofeq  6221  ofreq  6222  f1od2  6381  ovtposg  6405  recseq  6452  tfr2a  6467  rdgeq1  6517  rdgeq2  6518  freceq1  6538  freceq2  6539  eceq1  6715  eceq2  6717  qseq1  6730  qseq2  6731  uniqs  6740  ecinxp  6757  qsinxp  6758  erovlem  6774  ixpeq1  6856  supeq1  7153  supeq2  7156  supeq3  7157  supeq123d  7158  infeq1  7178  infeq2  7181  infeq3  7182  infeq123d  7183  infisoti  7199  djueq12  7206  acneq  7384  addpiord  7503  mulpiord  7504  00sr  7956  negeq  8339  csbnegg  8344  negsubdi  8402  mulneg1  8541  deceq1  9582  deceq2  9583  xnegeq  10023  fseq1p1m1  10290  frec2uzsucd  10623  frec2uzrdg  10631  frecuzrdgsuc  10636  frecuzrdgg  10638  frecuzrdgsuctlem  10645  seqeq1  10672  seqeq2  10673  seqeq3  10674  seqvalcd  10683  seq3f1olemp  10737  hashprg  11030  s1eq  11152  s1prc  11156  s2eqd  11302  s3eqd  11303  s4eqd  11304  s5eqd  11305  s6eqd  11306  s7eqd  11307  s8eqd  11308  shftdm  11333  resqrexlemfp1  11520  negfi  11739  sumeq1  11866  sumeq2  11870  zsumdc  11895  isumss2  11904  fsumsplitsnun  11930  isumclim3  11934  fisumcom2  11949  isumshft  12001  prodeq1f  12063  prodeq2w  12067  prodeq2  12068  zproddc  12090  fprodm1s  12112  fprodp1s  12113  fprodcom2fi  12137  fprodsplitf  12143  ege2le3  12182  efgt1p2  12206  dfphi2  12742  prmdiveq  12758  pceulem  12817  sloteq  13037  setsslid  13083  ressval2  13099  ecqusaddd  13775  ringidvalg  13924  zrhpropd  14590  metreslem  15054  comet  15173  cnmetdval  15203  dvmptfsum  15399  dvply1  15439  lgsdi  15716  lgseisenlem2  15750  lgsquadlem3  15758  uhgrvtxedgiedgb  15941  usgredg2v  16022  redcwlpolemeq1  16422