Theorem syl5req 1137

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

Ref	Expression
syl5req	⊢ (φ → B = C)

Proof of Theorem syl5req

Step	Hyp	Ref	Expression
1		syl5req.1	. . 3 ⊢ (φ → A = B)
2		syl5req.2	. . 3 ⊢ C = A
3	1, 2	syl5eq 1136	. 2 ⊢ (φ → C = B)
4	3	cleqcomd 1106	1 ⊢ (φ → B = C)

Syntax hints:   → wi 2   = wceq 1091

This theorem is referenced by:  syl5reqr 1139  onfr 2237  funcnvres 2710  fniunfv 2860  xpmapenlem4 3394  unblem2 3432  kmlem2 3581  kmlem10 3589  kmlem11 3590  1idsr 4001  rere 4810  bcs 5101  pjch 5269  shjshsel 5413

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