Theorem 3eqtr4g 2097

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

Syntax hints:   -> wi 4   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  rabeqf  2550  csbeq1  2855  csbeq2d  2874  csbnestgf  2898  difeq1  3055  difeq2  3056  uneq2  3091  ineq2  3132  dfrab3ss  3215  ifeq1  3334  ifeq2  3335  ifbi  3348  pweq  3362  sneq  3386  csbsng  3431  rabsn  3437  preq1  3447  preq2  3448  tpeq1  3456  tpeq2  3457  tpeq3  3458  prprc1  3478  opeq1  3549  opeq2  3550  oteq1  3558  oteq2  3559  oteq3  3560  csbunig  3588  unieq  3589  inteq  3618  iineq1  3671  iineq2  3674  dfiin2g  3690  iinrabm  3719  iinin1m  3726  iinxprg  3731  opabbid  3822  mpteq12f  3837  suceq  4139  xpeq1  4359  xpeq2  4360  csbxpg  4421  csbdmg  4529  rneq  4561  reseq1  4606  reseq2  4607  csbresg  4615  resmpt  4656  imaeq1  4663  imaeq2  4664  csbrng  4782  dmpropg  4793  rnpropg  4800  cores  4824  cores2  4833  xpcom  4864  iotaeq  4875  iotabi  4876  fntpg  4955  funimaexg  4983  fveq1  5177  fveq2  5178  fvres  5198  csbfv12g  5209  fnimapr  5233  fndmin  5274  fprg  5346  fsnunfv  5363  fsnunres  5364  fliftf  5439  isoini2  5458  riotaeqdv  5469  riotabidv  5470  riotauni  5474  riotabidva  5484  snriota  5497  oveq  5518  oveq1  5519  oveq2  5520  oprabbid  5558  mpt2eq123  5564  mpt2eq123dva  5566  mpt2eq3dva  5569  resmpt2  5599  ovres  5640  f1ocnvd  5702  ofeq  5714  ofreq  5715  ovtposg  5874  recseq  5921  tfr2a  5936  rdgeq1  5958  rdgeq2  5959  freceq1  5979  freceq2  5980  eceq1  6141  eceq2  6143  qseq1  6154  qseq2  6155  uniqs  6164  ecinxp  6181  qsinxp  6182  erovlem  6198  addpiord  6414  mulpiord  6415  00sr  6854  negeq  7204  csbnegg  7209  negsubdi  7267  mulneg1  7392  deceq1  8370  deceq2  8371  xnegeq  8740  fseq1p1m1  8956  frec2uzzd  9186  frec2uzsucd  9187  frec2uzrdg  9195  frecuzrdgsuc  9201  iseqeq1  9214  iseqeq2  9215  iseqeq3  9216  iseqeq4  9217  shftdm  9423  resqrexlemfp1  9607  sumeq1  9874