Theorem 3eqtr4g 2224

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	syl5eq 2211	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	eqtr4di 2217	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  rabbidva2  2713  rabeqf  2716  csbeq1  3048  csbeq2  3069  csbeq2d  3070  csbnestgf  3097  difeq1  3233  difeq2  3234  uneq2  3270  ineq2  3317  dfrab3ss  3400  ifeq1  3523  ifeq2  3524  ifbi  3540  pweq  3562  sneq  3587  csbsng  3637  rabsn  3643  preq1  3653  preq2  3654  tpeq1  3662  tpeq2  3663  tpeq3  3664  prprc1  3684  opeq1  3758  opeq2  3759  oteq1  3767  oteq2  3768  oteq3  3769  csbunig  3797  unieq  3798  inteq  3827  iineq1  3880  iineq2  3883  dfiin2g  3899  iinrabm  3928  iinin1m  3935  iinxprg  3940  opabbid  4047  mpteq12f  4062  suceq  4380  xpeq1  4618  xpeq2  4619  csbxpg  4685  csbdmg  4798  rneq  4831  reseq1  4878  reseq2  4879  csbresg  4887  resindm  4926  resmpt  4932  resmptf  4934  imaeq1  4941  imaeq2  4942  mptcnv  5006  csbrng  5065  dmpropg  5076  rnpropg  5083  cores  5107  cores2  5116  xpcom  5150  iotaeq  5161  iotabi  5162  fntpg  5244  funimaexg  5272  fveq1  5485  fveq2  5486  fvres  5510  csbfv12g  5522  fnimapr  5546  fndmin  5592  fprg  5668  fsnunfv  5686  fsnunres  5687  fliftf  5767  isoini2  5787  riotaeqdv  5799  riotabidv  5800  riotauni  5804  riotabidva  5814  snriota  5827  oveq  5848  oveq1  5849  oveq2  5850  oprabbid  5895  mpoeq123  5901  mpoeq123dva  5903  mpoeq3dva  5906  resmpo  5940  ovres  5981  f1ocnvd  6040  ofeq  6052  ofreq  6053  f1od2  6203  ovtposg  6227  recseq  6274  tfr2a  6289  rdgeq1  6339  rdgeq2  6340  freceq1  6360  freceq2  6361  eceq1  6536  eceq2  6538  qseq1  6549  qseq2  6550  uniqs  6559  ecinxp  6576  qsinxp  6577  erovlem  6593  ixpeq1  6675  supeq1  6951  supeq2  6954  supeq3  6955  supeq123d  6956  infeq1  6976  infeq2  6979  infeq3  6980  infeq123d  6981  infisoti  6997  djueq12  7004  addpiord  7257  mulpiord  7258  00sr  7710  negeq  8091  csbnegg  8096  negsubdi  8154  mulneg1  8293  deceq1  9326  deceq2  9327  xnegeq  9763  fseq1p1m1  10029  frec2uzsucd  10336  frec2uzrdg  10344  frecuzrdgsuc  10349  frecuzrdgg  10351  frecuzrdgsuctlem  10358  seqeq1  10383  seqeq2  10384  seqeq3  10385  seqvalcd  10394  seq3f1olemp  10437  hashprg  10721  shftdm  10764  resqrexlemfp1  10951  negfi  11169  sumeq1  11296  sumeq2  11300  zsumdc  11325  isumss2  11334  fsumsplitsnun  11360  isumclim3  11364  fisumcom2  11379  isumshft  11431  prodeq1f  11493  prodeq2w  11497  prodeq2  11498  zproddc  11520  fprodm1s  11542  fprodp1s  11543  fprodcom2fi  11567  fprodsplitf  11573  ege2le3  11612  efgt1p2  11636  dfphi2  12152  prmdiveq  12168  pceulem  12226  sloteq  12399  setsslid  12444  metreslem  13020  comet  13139  cnmetdval  13169  lgsdi  13578  redcwlpolemeq1  13933