Theorem 3eqtr4g 1531

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

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  rabbidv 1806  rabeqf 1808  csbeq1 2003  csbcog 2007  difeq1 2153  difeq2 2154  uneq2 2178  ineq2 2211  ifeq1 2364  ifeq2 2365  pweq 2403  sneq 2417  rabsn 2445  preq1 2448  preq2 2449  prprc1 2452  opeq1 2487  opeq2 2488  opprc2 2499  unieq 2510  inteq 2536  iineq1 2576  iineq2 2579  dfiun2g 2586  opabbid 2669  suceq 3034  xpeq1 3200  xpeq2 3201  coeq1 3281  coeq2 3282  dmsnop 3328  rneq 3339  reseq1 3368  reseq2 3369  imaeq1 3401  imaeq2 3402  cores2 3507  fveq1 3723  fveq2 3724  fvres 3734  rdgeq1 3934  rdgeq2 3935  abianfplem 3961  opreq 3967  opreq1 3968  opreq2 3969  oprprc2 3985  oprabbid 3995  oprvalres 4033  oarec 4196  eceq1 4277  eceq2 4278  qseq1 4288  qseq2 4289  ecopoprtrn 4311  ixpeq1 4353  supeq1 4575  inf3lemc 4611  r1lim 4653  karden 4726  aceq6a 4741  zorn2lem1 4788  zorn2lem7 4794  zorn2 4796  cardiun 4859  alephlim 4864  addpiord 5012  mulpiord 5013  addcmpblnq 5052  ordpipq 5056  mulidpq 5069  ltsrpr 5186  00sr 5208  recexsrlem 5212  mulgt0sr 5214  addcnsrec 5263  mulcnsrec 5264  negeq 5359  eqneg 5804  supxrre 6083  ser1add2 6338  ser1add 6339  iooval2t 6367  icoshftf1olem 6410  sumeq1 6982  sumeq2 6985  fsump1f 7011  ser0mulc 7059  ser1mulc 7060  isumnn0nn 7207  isumnn0nna 7208  isummulc1a 7214  fsum0diag2 7259  efcltlem2 7305  acdc2lem2 7489  acdc5lem2 7492  cnmetdval 7902  imsdval 8317  avril1 8784  bcseq 8986  normpyth 9009  occllem5 9177  pjthlem6 9224  pjmvalt 9238  cm0t 9552  fh1t 9561  pjcj 9629  pjsdi2 10085  pjclem3 10125  pjc 10128  golem1 10198  ee7.2a 10425

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain