Theorem 3eqtr4g 2094

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

Syntax hints:   -> wi 4   = wceq 1242

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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

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

This theorem is referenced by:  rabeqf  2544  csbeq1  2849  csbeq2d  2868  csbnestgf  2892  difeq1  3049  difeq2  3050  uneq2  3085  ineq2  3126  dfrab3ss  3209  ifeq1  3328  ifeq2  3329  ifbi  3342  pweq  3354  sneq  3378  csbsng  3422  rabsn  3428  preq1  3438  preq2  3439  tpeq1  3447  tpeq2  3448  tpeq3  3449  prprc1  3469  opeq1  3540  opeq2  3541  oteq1  3549  oteq2  3550  oteq3  3551  csbunig  3579  unieq  3580  inteq  3609  iineq1  3662  iineq2  3665  dfiin2g  3681  iinrabm  3710  iinin1m  3717  iinxprg  3722  opabbid  3813  mpteq12f  3828  suceq  4105  xpeq1  4302  xpeq2  4303  csbxpg  4364  csbdmg  4472  rneq  4504  reseq1  4549  reseq2  4550  csbresg  4558  resmpt  4599  imaeq1  4606  imaeq2  4607  csbrng  4725  dmpropg  4736  rnpropg  4743  cores  4767  cores2  4776  xpcom  4807  iotaeq  4818  iotabi  4819  fntpg  4898  funimaexg  4926  fveq1  5120  fveq2  5121  fvres  5141  csbfv12g  5152  fnimapr  5176  fndmin  5217  fprg  5289  fsnunfv  5306  fsnunres  5307  fliftf  5382  isoini2  5401  riotaeqdv  5412  riotabidv  5413  riotauni  5417  riotabidva  5427  snriota  5440  oveq  5461  oveq1  5462  oveq2  5463  oprabbid  5500  mpt2eq123  5506  mpt2eq123dva  5508  mpt2eq3dva  5511  resmpt2  5541  ovres  5582  f1ocnvd  5644  ofeq  5656  ofreq  5657  ovtposg  5815  recseq  5862  tfr2a  5877  rdgeq1  5898  rdgeq2  5899  freceq1  5919  freceq2  5920  eceq1  6077  eceq2  6079  qseq1  6090  qseq2  6091  uniqs  6100  ecinxp  6117  qsinxp  6118  erovlem  6134  addpiord  6300  mulpiord  6301  00sr  6697  negeq  7001  csbnegg  7006  negsubdi  7063  mulneg1  7188  deceq1  8146  deceq2  8147  xnegeq  8510  fseq1p1m1  8726  frec2uzzd  8867  frec2uzsucd  8868  frec2uzrdg  8876  frecuzrdgsuc  8882  iseqeq1  8894  iseqeq2  8895  iseqeq3  8896  iseqeq4  8897