Theorem 3eqtr4g 1574

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

Syntax hints:   -> wi 3   = wceq 992

This theorem is referenced by:  rabbidv 1852  rabeqf 1854  csbeq1 2053  cbvcsbv 2054  csbcog 2058  difeq1 2205  difeq2 2206  uneq2 2230  ineq2 2263  ifeq1 2418  ifeq2 2419  pweq 2460  sneq 2475  rabsn 2506  preq1 2509  preq2 2510  prprc1 2515  opeq1 2552  opeq2 2553  opprc2 2564  unieq 2576  inteq 2603  iineq1 2644  iineq2 2647  dfiun2g 2654  opabbid 2743  suceq 3038  xpeq1 3281  xpeq2 3282  coeq1 3371  coeq2 3372  rneq 3426  reseq1 3455  reseq2 3456  imaeq1 3491  imaeq2 3492  dmsnop 3577  cores2 3611  imain 3680  fveq1 3834  fveq2 3835  fvres 3845  opreq 4025  opreq1 4026  opreq2 4027  oprprc2 4043  oprabbid 4054  oprvres 4094  onopruni 4210  onopriun 4211  rdgeq1 4235  rdgeq2 4236  abianfplem 4262  oarec 4332  eceq1 4417  eceq2 4418  qseq1 4428  qseq2 4429  ecopoprtrn 4452  ixpeq1 4494  supeq1 4718  inf3lemc 4756  r1lim 4799  karden 4872  aceq6a 4887  zorn2lem1 4934  zorn2lem7 4940  zorn2 4942  cardiun 5009  alephlim 5014  addpiord 5166  mulpiord 5167  addcmpblnq 5206  ordpipq 5210  mulidpq 5223  ltsrpr 5340  00sr 5362  recexsrlem 5366  mulgt0sr 5368  addcnsrec 5417  mulcnsrec 5418  negeq 5513  eqnegi 5944  supxrre 6251  iooval2 6493  icoshftf1olem 6537  ser1add2i 6703  ser1addi 6704  sumeq1 7185  sumeq2 7188  fsump1fi 7214  ser0mulci 7262  ser1mulci 7263  isumnn0nn 7411  isumnn0nnai 7412  isummulc1ai 7418  fsum0diag2 7464  efcltlem2 7510  acdc2lem2 7701  acdc5lem2 7704  cnmetdval 8113  imsdval 8564  avril1 9058  bcseqi 9262  normpythi 9285  occllem5 9453  pjthlem6 9500  pjmval 9514  cm0 9828  fh1 9837  pjcji 9907  pjsdi2i 10365  pjclem3 10406  pjci 10409  golem1 10479  ee7.2a 10710  oprssoprvg 10818  dfiin2g 11400  ordtypelem1 11427  ordtypelem4 11430  ordtypelem5 11431  ordtypelem6 11432  ordtypelem7 11433  ordtype 11434  flimfnfcls 11727  gaid 11776  ssga 11777  supeq2 11852  totbndbnd 12000

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain