Theorem 3eqtr4g 1534

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

Hypotheses

Ref	Expression
3eqtr4g.1	⊢ (φ → A = B)
3eqtr4g.2	⊢ C = A
3eqtr4g.3	⊢ D = B

Assertion

Ref	Expression
3eqtr4g	⊢ (φ → C = D)

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.1	. . 3 ⊢ (φ → A = B)
2		3eqtr4g.2	. . 3 ⊢ C = A
3	1, 2	syl5eq 1522	. 2 ⊢ (φ → C = B)
4		3eqtr4g.3	. 2 ⊢ D = B
5	3, 4	syl6eqr 1528	1 ⊢ (φ → C = D)

Syntax hints:   → wi 3   = wceq 958

This theorem is referenced by:  rabbidv 1809  rabeqf 1811  csbeq1 2006  csbcog 2010  difeq1 2156  difeq2 2157  uneq2 2181  ineq2 2214  ifeq1 2368  ifeq2 2369  pweq 2407  sneq 2421  rabsn 2449  preq1 2452  preq2 2453  prprc1 2456  opeq1 2491  opeq2 2492  opprc2 2503  unieq 2514  inteq 2540  iineq1 2580  iineq2 2583  dfiun2g 2590  opabbid 2674  suceq 3040  xpeq1 3206  xpeq2 3207  coeq1 3287  coeq2 3288  dmsnop 3334  rneq 3345  reseq1 3374  reseq2 3375  imaeq1 3407  imaeq2 3408  cores2 3513  fveq1 3729  fveq2 3730  fvres 3740  rdgeq1 3940  rdgeq2 3941  abianfplem 3967  opreq 3973  opreq1 3974  opreq2 3975  oprprc2 3991  oprabbid 4001  oprvalres 4039  oarec 4202  eceq1 4283  eceq2 4284  qseq1 4294  qseq2 4295  ecopoprtrn 4317  ixpeq1 4359  supeq1 4584  inf3lemc 4620  r1lim 4663  karden 4736  aceq6a 4751  zorn2lem1 4798  zorn2lem7 4804  zorn2 4806  cardiun 4870  alephlim 4875  addpiord 5024  mulpiord 5025  addcmpblnq 5064  ordpipq 5068  mulidpq 5081  ltsrpr 5198  00sr 5220  recexsrlem 5224  mulgt0sr 5226  addcnsrec 5275  mulcnsrec 5276  negeq 5371  eqneg 5806  supxrre 6085  ser1add2 6339  ser1add 6340  iooval2t 6368  icoshftf1olem 6411  sumeq1 6982  sumeq2 6985  fsump1f 7011  ser0mulc 7059  ser1mulc 7060  isumnn0nn 7207  isumnn0nna 7208  isummulc1a 7214  fsum0diag2 7259  efcltlem2 7305  acdc2lem2 7490  acdc5lem2 7493  cnmetdval 7899  imsdval 8313  avril1 8779  bcseq 8981  normpyth 9004  occllem5 9172  pjthlem6 9219  pjmvalt 9233  cm0t 9547  fh1t 9556  pjcj 9624  pjsdi2 10080  pjclem3 10120  pjc 10123  golem1 10193  ee7.2a 10420

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