Theorem 3eqtr4g 1147

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

Syntax hints:   -> wi 2   = wceq 1091

This theorem is referenced by:  birabdv 1343  rabeqf 1345  difeq1 1582  difeq2 1583  uneq2 1606  ineq2 1639  ifeq1 1778  ifeq2 1779  pweq 1800  sneq 1816  prprc 1839  preq1 1870  preq2 1871  opeq1 1876  opeq2 1877  opprc2 1907  unieq 1927  inteq 1968  iineq1 2004  iineq2 2007  biopabd 2101  supeq1 2155  suceq 2288  xpeq1 2440  xpeq2 2441  coeq1 2502  coeq2 2503  dmsnop 2547  rneq 2555  reseq1 2575  reseq2 2576  resabs1 2592  resabs2 2593  imaeq1 2602  imaeq2 2603  fveq1 2831  fveq2 2832  fvres 2840  tfrlem10 2958  rdgeq1 2972  rdgeq2 2973  abianfplem 2999  opreq 3005  opreq1 3006  opreq2 3007  oprprc2 3020  bioprabd 3025  eceq1 3214  eceq2 3215  qseq1 3225  qseq2 3226  ecopoprtrn 3247  inf3lemc 3462  r1lim 3497  karden 3551  aceq6a 3564  zornlem1 3603  zornlem7 3609  zorn 3611  cardiun 3665  alephlim 3670  addpiord 3806  mulpiord 3807  addcmpblnq 3846  ordpipq 3850  mulidpq 3863  ltsrpr 3980  00sr 4002  recexsrlem 4006  mulgt0sr 4008  addcnsrec 4057  mulcnsrec 4058  axrecex 4079  negeq 4136  eqneg 4378  reim0 4809  bcseq 5073  normpyth 5090  occllem5 5184  pjthlem6 5230  pjmvalt 5245  pjcj 5575  pjsdi2 5627  pjclem3 5651  pjc 5654  golem1 5704

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org