Theorem 3eqtr4g 2247

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

Syntax hints:   -> wi 4   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182

This theorem is referenced by:  rabbidva2  2739  rabeqf  2742  csbeq1  3075  csbeq2  3096  csbeq2d  3097  csbnestgf  3124  difeq1  3261  difeq2  3262  uneq2  3298  ineq2  3345  dfrab3ss  3428  ifeq1  3552  ifeq2  3553  ifbi  3569  pweq  3596  sneq  3621  csbsng  3671  rabsn  3677  preq1  3687  preq2  3688  tpeq1  3696  tpeq2  3697  tpeq3  3698  prprc1  3718  opeq1  3796  opeq2  3797  oteq1  3805  oteq2  3806  oteq3  3807  csbunig  3835  unieq  3836  inteq  3865  iineq1  3918  iineq2  3921  dfiin2g  3937  iinrabm  3967  iinin1m  3974  iinxprg  3979  opabbid  4086  mpteq12f  4101  suceq  4423  xpeq1  4661  xpeq2  4662  csbxpg  4728  csbdmg  4842  rneq  4875  reseq1  4922  reseq2  4923  csbresg  4931  resindm  4970  resmpt  4976  resmptf  4978  imaeq1  4986  imaeq2  4987  mptcnv  5052  csbrng  5111  dmpropg  5122  rnpropg  5129  cores  5153  cores2  5162  xpcom  5196  iotaeq  5207  iotabi  5208  fntpg  5294  funimaexg  5322  fveq1  5536  fveq2  5537  fvres  5561  csbfv12g  5575  fnimapr  5600  fndmin  5647  fprg  5723  fsnunfv  5741  fsnunres  5742  fliftf  5824  isoini2  5844  riotaeqdv  5856  riotabidv  5857  riotauni  5862  riotabidva  5872  snriota  5885  oveq  5906  oveq1  5907  oveq2  5908  oprabbid  5953  mpoeq123  5959  mpoeq123dva  5961  mpoeq3dva  5964  resmpo  5998  ovres  6040  f1ocnvd  6100  ofeqd  6112  ofeq  6113  ofreq  6114  f1od2  6264  ovtposg  6288  recseq  6335  tfr2a  6350  rdgeq1  6400  rdgeq2  6401  freceq1  6421  freceq2  6422  eceq1  6598  eceq2  6600  qseq1  6613  qseq2  6614  uniqs  6623  ecinxp  6640  qsinxp  6641  erovlem  6657  ixpeq1  6739  supeq1  7019  supeq2  7022  supeq3  7023  supeq123d  7024  infeq1  7044  infeq2  7047  infeq3  7048  infeq123d  7049  infisoti  7065  djueq12  7072  addpiord  7350  mulpiord  7351  00sr  7803  negeq  8186  csbnegg  8191  negsubdi  8249  mulneg1  8388  deceq1  9424  deceq2  9425  xnegeq  9864  fseq1p1m1  10131  frec2uzsucd  10439  frec2uzrdg  10447  frecuzrdgsuc  10452  frecuzrdgg  10454  frecuzrdgsuctlem  10461  seqeq1  10488  seqeq2  10489  seqeq3  10490  seqvalcd  10499  seq3f1olemp  10542  hashprg  10830  shftdm  10873  resqrexlemfp1  11060  negfi  11278  sumeq1  11405  sumeq2  11409  zsumdc  11434  isumss2  11443  fsumsplitsnun  11469  isumclim3  11473  fisumcom2  11488  isumshft  11540  prodeq1f  11602  prodeq2w  11606  prodeq2  11607  zproddc  11629  fprodm1s  11651  fprodp1s  11652  fprodcom2fi  11676  fprodsplitf  11682  ege2le3  11721  efgt1p2  11745  dfphi2  12264  prmdiveq  12280  pceulem  12338  sloteq  12529  setsslid  12575  ressval2  12590  ecqusaddd  13203  ringidvalg  13341  metreslem  14366  comet  14485  cnmetdval  14515  lgsdi  14942  lgseisenlem2  14955  redcwlpolemeq1  15308