Theorem 3eqtr4g 1534

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

Syntax hints:   -> wi 3   = wceq 958

This theorem is referenced by:  rabbidv 1809  rabeqf 1811  csbeq1 2007  csbcog 2011  difeq1 2157  difeq2 2158  uneq2 2182  ineq2 2215  ifeq1 2369  ifeq2 2370  pweq 2408  sneq 2422  rabsn 2450  preq1 2453  preq2 2454  prprc1 2457  opeq1 2492  opeq2 2493  opprc2 2504  unieq 2515  inteq 2541  iineq1 2581  iineq2 2584  dfiun2g 2591  opabbid 2675  suceq 3041  xpeq1 3207  xpeq2 3208  coeq1 3288  coeq2 3289  dmsnop 3335  rneq 3346  reseq1 3375  reseq2 3376  imaeq1 3408  imaeq2 3409  cores2 3514  fveq1 3730  fveq2 3731  fvres 3741  rdgeq1 3941  rdgeq2 3942  abianfplem 3968  opreq 3974  opreq1 3975  opreq2 3976  oprprc2 3992  oprabbid 4002  oprvalres 4040  oarec 4203  eceq1 4284  eceq2 4285  qseq1 4295  qseq2 4296  ecopoprtrn 4318  ixpeq1 4360  supeq1 4591  inf3lemc 4627  r1lim 4670  karden 4743  aceq6a 4758  zorn2lem1 4805  zorn2lem7 4811  zorn2 4813  cardiun 4877  alephlim 4882  addpiord 5031  mulpiord 5032  addcmpblnq 5071  ordpipq 5075  mulidpq 5088  ltsrpr 5205  00sr 5227  recexsrlem 5231  mulgt0sr 5233  addcnsrec 5282  mulcnsrec 5283  negeq 5378  eqneg 5813  supxrre 6092  ser1add2 6346  ser1add 6347  iooval2t 6375  icoshftf1olem 6418  sumeq1 6989  sumeq2 6992  fsump1f 7018  ser0mulc 7066  ser1mulc 7067  isumnn0nn 7214  isumnn0nna 7215  isummulc1a 7221  fsum0diag2 7266  efcltlem2 7312  acdc2lem2 7497  acdc5lem2 7500  cnmetdval 7906  imsdval 8320  avril1 8786  bcseq 8988  normpyth 9011  occllem5 9179  pjthlem6 9226  pjmvalt 9240  cm0t 9554  fh1t 9563  pjcj 9631  pjsdi2 10087  pjclem3 10128  pjc 10131  golem1 10201  ee7.2a 10428

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain