Theorem 3eqtr4g 2138

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 2125	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	syl6eqr 2131	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  rabeqf  2594  csbeq1  2911  csbeq2d  2930  csbnestgf  2954  difeq1  3083  difeq2  3084  uneq2  3120  ineq2  3161  dfrab3ss  3242  ifeq1  3354  ifeq2  3355  ifbi  3369  pweq  3385  sneq  3409  csbsng  3453  rabsn  3459  preq1  3469  preq2  3470  tpeq1  3478  tpeq2  3479  tpeq3  3480  prprc1  3500  opeq1  3570  opeq2  3571  oteq1  3579  oteq2  3580  oteq3  3581  csbunig  3609  unieq  3610  inteq  3639  iineq1  3692  iineq2  3695  dfiin2g  3711  iinrabm  3740  iinin1m  3747  iinxprg  3752  opabbid  3843  mpteq12f  3858  suceq  4157  xpeq1  4377  xpeq2  4378  csbxpg  4439  csbdmg  4547  rneq  4579  reseq1  4624  reseq2  4625  csbresg  4633  resindm  4670  resmpt  4676  imaeq1  4683  imaeq2  4684  csbrng  4802  dmpropg  4813  rnpropg  4820  cores  4844  cores2  4853  xpcom  4884  iotaeq  4895  iotabi  4896  fntpg  4975  funimaexg  5003  fveq1  5197  fveq2  5198  fvres  5219  csbfv12g  5230  fnimapr  5254  fndmin  5295  fprg  5367  fsnunfv  5384  fsnunres  5385  fliftf  5459  isoini2  5478  riotaeqdv  5489  riotabidv  5490  riotauni  5494  riotabidva  5504  snriota  5517  oveq  5538  oveq1  5539  oveq2  5540  oprabbid  5578  mpt2eq123  5584  mpt2eq123dva  5586  mpt2eq3dva  5589  resmpt2  5619  ovres  5660  f1ocnvd  5722  ofeq  5734  ofreq  5735  f1od2  5876  ovtposg  5897  recseq  5944  tfr2a  5959  rdgeq1  5981  rdgeq2  5982  freceq1  6002  freceq2  6003  eceq1  6164  eceq2  6166  qseq1  6177  qseq2  6178  uniqs  6187  ecinxp  6204  qsinxp  6205  erovlem  6221  supeq1  6399  supeq2  6402  supeq3  6403  supeq123d  6404  infeq1  6424  infeq2  6427  infeq3  6428  infeq123d  6429  infisoti  6445  addpiord  6506  mulpiord  6507  00sr  6946  negeq  7301  csbnegg  7306  negsubdi  7364  mulneg1  7499  deceq1  8481  deceq2  8482  xnegeq  8894  fseq1p1m1  9111  frec2uzzd  9402  frec2uzsucd  9403  frec2uzrdg  9411  frecuzrdgsuc  9417  iseqeq1  9434  iseqeq2  9435  iseqeq3  9436  iseqeq4  9437  shftdm  9710  resqrexlemfp1  9895  negfi  10110  sumeq1  10192