Theorem 3eqtr4g 2172

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

Syntax hints:   -> wi 4   = wceq 1314

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097

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

This theorem is referenced by:  rabbidva2  2644  rabeqf  2647  csbeq1  2974  csbeq2d  2993  csbnestgf  3018  difeq1  3153  difeq2  3154  uneq2  3190  ineq2  3237  dfrab3ss  3320  ifeq1  3443  ifeq2  3444  ifbi  3458  pweq  3479  sneq  3504  csbsng  3550  rabsn  3556  preq1  3566  preq2  3567  tpeq1  3575  tpeq2  3576  tpeq3  3577  prprc1  3597  opeq1  3671  opeq2  3672  oteq1  3680  oteq2  3681  oteq3  3682  csbunig  3710  unieq  3711  inteq  3740  iineq1  3793  iineq2  3796  dfiin2g  3812  iinrabm  3841  iinin1m  3848  iinxprg  3853  opabbid  3953  mpteq12f  3968  suceq  4284  xpeq1  4513  xpeq2  4514  csbxpg  4580  csbdmg  4693  rneq  4726  reseq1  4771  reseq2  4772  csbresg  4780  resindm  4819  resmpt  4825  resmptf  4827  imaeq1  4834  imaeq2  4835  mptcnv  4899  csbrng  4958  dmpropg  4969  rnpropg  4976  cores  5000  cores2  5009  xpcom  5043  iotaeq  5054  iotabi  5055  fntpg  5137  funimaexg  5165  fveq1  5374  fveq2  5375  fvres  5399  csbfv12g  5411  fnimapr  5435  fndmin  5481  fprg  5557  fsnunfv  5575  fsnunres  5576  fliftf  5654  isoini2  5674  riotaeqdv  5685  riotabidv  5686  riotauni  5690  riotabidva  5700  snriota  5713  oveq  5734  oveq1  5735  oveq2  5736  oprabbid  5778  mpoeq123  5784  mpoeq123dva  5786  mpoeq3dva  5789  resmpo  5823  ovres  5864  f1ocnvd  5926  ofeq  5938  ofreq  5939  f1od2  6086  ovtposg  6110  recseq  6157  tfr2a  6172  rdgeq1  6222  rdgeq2  6223  freceq1  6243  freceq2  6244  eceq1  6418  eceq2  6420  qseq1  6431  qseq2  6432  uniqs  6441  ecinxp  6458  qsinxp  6459  erovlem  6475  ixpeq1  6557  supeq1  6825  supeq2  6828  supeq3  6829  supeq123d  6830  infeq1  6850  infeq2  6853  infeq3  6854  infeq123d  6855  infisoti  6871  djueq12  6876  addpiord  7072  mulpiord  7073  00sr  7512  negeq  7878  csbnegg  7883  negsubdi  7941  mulneg1  8076  deceq1  9090  deceq2  9091  xnegeq  9503  fseq1p1m1  9767  frec2uzsucd  10067  frec2uzrdg  10075  frecuzrdgsuc  10080  frecuzrdgg  10082  frecuzrdgsuctlem  10089  seqeq1  10114  seqeq2  10115  seqeq3  10116  seqvalcd  10125  seq3f1olemp  10168  hashprg  10447  shftdm  10487  resqrexlemfp1  10673  negfi  10891  sumeq1  11016  sumeq2  11020  zsumdc  11045  isumss2  11054  fsumsplitsnun  11080  isumclim3  11084  fisumcom2  11099  isumshft  11151  ege2le3  11228  efgt1p2  11252  dfphi2  11741  sloteq  11807  setsslid  11852  metreslem  12369  comet  12488  cnmetdval  12518