Theorem 3eqtr4g 1578

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

Syntax hints:   -> wi 3   = wceq 997

This theorem is referenced by:  rabbidv 1853  rabeqf 1855  csbeq1 2053  cbvcsbv 2054  csbcog 2058  difeq1 2204  difeq2 2205  uneq2 2229  ineq2 2262  ifeq1 2416  ifeq2 2417  pweq 2455  sneq 2469  rabsn 2497  preq1 2500  preq2 2501  prprc1 2506  opeq1 2541  opeq2 2542  opprc2 2553  unieq 2564  inteq 2590  iineq1 2630  iineq2 2633  dfiun2g 2640  opabbid 2724  suceq 3091  xpeq1 3257  xpeq2 3258  coeq1 3338  coeq2 3339  dmsnop 3385  rneq 3396  reseq1 3425  reseq2 3426  imaeq1 3458  imaeq2 3459  cores2 3564  fveq1 3780  fveq2 3781  fvres 3791  rdgeq1 3992  rdgeq2 3993  abianfplem 4019  opreq 4025  opreq1 4026  opreq2 4027  oprprc2 4043  oprabbid 4053  oprvalres 4091  oarec 4254  eceq1 4335  eceq2 4336  qseq1 4346  qseq2 4347  ecopoprtrn 4372  ixpeq1 4414  supeq1 4635  inf3lemc 4673  r1lim 4715  karden 4788  aceq6a 4803  zorn2lem1 4850  zorn2lem7 4856  zorn2 4858  cardiun 4924  alephlim 4929  addpiord 5077  mulpiord 5078  addcmpblnq 5117  ordpipq 5121  mulidpq 5134  ltsrpr 5251  00sr 5273  recexsrlem 5277  mulgt0sr 5279  addcnsrec 5328  mulcnsrec 5329  negeq 5424  eqnegi 5862  supxrre 6165  iooval2 6392  icoshftf1olem 6436  ser1add2i 6597  ser1addi 6598  sumeq1 7072  sumeq2 7075  fsump1fi 7101  ser0mulci 7149  ser1mulci 7150  isumnn0nn 7297  isumnn0nnai 7298  isummulc1ai 7304  fsum0diag2 7349  efcltlem2 7395  acdc2lem2 7581  acdc5lem2 7584  cnmetdval 7987  imsdval 8401  avril1 8867  bcseqi 9069  normpythi 9092  occllem5 9260  pjthlem6 9307  pjmval 9321  cm0 9635  fh1 9644  pjcji 9712  pjsdi2i 10168  pjclem3 10209  pjci 10212  golem1 10282  ee7.2a 10512

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-cleq 1515

Copyright terms: Public domain