Theorem 3eqtr4g 1528

Description: A chained equality inference, useful for converting to definitions.

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

Syntax hints:   -> wi 3   = wceq 954

This theorem is referenced by:  rabbidv 1802  rabeqf 1804  csbeq1 1999  csbcog 2003  difeq1 2149  difeq2 2150  uneq2 2174  ineq2 2207  ifeq1 2360  ifeq2 2361  pweq 2399  sneq 2413  rabsn 2441  preq1 2444  preq2 2445  prprc1 2448  opeq1 2483  opeq2 2484  opprc2 2495  unieq 2505  inteq 2531  iineq1 2571  iineq2 2574  dfiun2g 2581  opabbid 2664  suceq 3029  xpeq1 3195  xpeq2 3196  coeq1 3276  coeq2 3277  dmsnop 3323  rneq 3334  reseq1 3360  reseq2 3361  imaeq1 3393  imaeq2 3394  cores2 3499  fveq1 3714  fveq2 3715  fvres 3725  rdgeq1 3925  rdgeq2 3926  abianfplem 3952  opreq 3958  opreq1 3959  opreq2 3960  oprprc2 3976  oprabbid 3986  oprvalres 4024  oarec 4186  eceq1 4267  eceq2 4268  qseq1 4278  qseq2 4279  ecopoprtrn 4301  ixpeq1 4343  supeq1 4555  inf3lemc 4591  r1lim 4633  karden 4706  aceq6a 4721  zorn2lem1 4768  zorn2lem7 4774  zorn2 4776  cardiun 4839  alephlim 4844  addpiord 4992  mulpiord 4993  addcmpblnq 5032  ordpipq 5036  mulidpq 5049  ltsrpr 5166  00sr 5188  recexsrlem 5192  mulgt0sr 5194  addcnsrec 5243  mulcnsrec 5244  negeq 5339  eqneg 5768  supxrre 6038  ser1add2 6283  ser1add 6284  iooval2t 6312  icoshftf1olem 6351  sumeq1 6928  sumeq2 6931  fsump1f 6957  ser0mulc 7005  ser1mulc 7006  isumnn0nn 7150  isumnn0nna 7151  isummulc1a 7157  fsum0diag2 7202  efcltlem2 7255  acdc2lem2 7439  acdc5lem2 7442  cnmetdval 7854  imsdval 8268  avril1 8723  bcseq 8925  normpyth 8948  occllem5 9116  pjthlem6 9162  pjmvalt 9176  cm0t 9492  fh1t 9501  pjcj 9569  pjsdi2 10023  pjclem3 10063  pjc 10066  golem1 10136  ee7.2a 10361

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467

Copyright terms: Public domain