Theorem syl6eqr 1142

Description: An equality transitivity deduction.

Hypotheses

Ref	Expression
syl6eqr.1	⊢ (φ → A = B)
syl6eqr.2	⊢ C = B

Assertion

Ref	Expression
syl6eqr	⊢ (φ → A = C)

Proof of Theorem syl6eqr

Step	Hyp	Ref	Expression
1		syl6eqr.1	. 2 ⊢ (φ → A = B)
2		syl6eqr.2	. . 3 ⊢ C = B
3	2	cleqcomi 1105	. 2 ⊢ B = C
4	1, 3	syl6eq 1140	1 ⊢ (φ → A = C)

Syntax hints:   → wi 2   = wceq 1091

This theorem is referenced by:  3eqtr4g 1147  opprc3 1908  rdglim2a 2988  ffnoprval 3041  fnoprval 3042  oprvalex 3055  oa0r 3141  om1r 3145  xpmapenlem3 3393  xpmapenlem5 3395  phplem2 3404  zornlem1 3603  halfpq 3876  prlem934a 3931  prlem936 3949  mulcmpblnrlem 3976  recexsrlem 4006  axnegex 4078  axrecex 4079  seqval 4665  nneo 4719  pjthlem7 5231  stm1add 5686  stm1add3 5688

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