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  3145  ssdifeq0  3633  pw1equn  4332  sfinltfin  4536  vfintle  4547  phialllem2  4618  opabbi2dv  4868  fcoi1  5241  f1imacnv  5303  foimacnv  5304  f1ococnv1  5311  funfv  5376  fsn2  5435  funiunfvf  5469  f1ocnvfv2  5478  brcomposeg  5820  mapsn  6027  enpw1  6063  enmap2  6069  enmap1lem5  6074  ncdisjun  6137