Theorem syl5eqr 2399

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
syl5eqr	⊢ (φ → A = C)

Proof of Theorem syl5eqr

Step	Hyp	Ref	Expression
1		syl5eqr.1	. . 3 ⊢ B = A
2	1	eqcomi 2357	. 2 ⊢ A = B
3		syl5eqr.2	. 2 ⊢ (φ → B = C)
4	2, 3	syl5eq 2397	1 ⊢ (φ → A = C)

Syntax hints:   → wi 4   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  3eqtr3g  2408  csbeq1a  3144  ssdifeq0  3632  pw1equn  4331  sfinltfin  4535  vfintle  4546  phialllem2  4617  opabbi2dv  4867  fcoi1  5240  f1imacnv  5302  foimacnv  5303  f1ococnv1  5310  funfv  5375  fsn2  5434  funiunfvf  5468  f1ocnvfv2  5477  brcomposeg  5819  mapsn  6026  enpw1  6062  enmap2  6068  enmap1lem5  6073  ncdisjun  6136