Theorem syl5reqr 2136

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
syl5reqr.1	|- B = A
syl5reqr.2	|- ( ph -> B = C )

Assertion

Ref	Expression
syl5reqr	|- ( ph -> C = A )

Proof of Theorem syl5reqr

Step	Hyp	Ref	Expression
1		syl5reqr.1	. . 3 |- B = A
2	1	eqcomi 2093	. 2 |- A = B
3		syl5reqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5req 2134	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1290

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-4 1446  ax-17 1465  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-cleq 2082

This theorem is referenced by:  bm2.5ii  4326  resdmdfsn  4768  f0dom0  5217  f1o00  5301  fmpt  5463  fmptsn  5500  resfunexg  5532  mapsn  6461  sbthlemi4  6723  sbthlemi6  6725  pm54.43  6879  prarloclem5  7120  recexprlem1ssl  7253  recexprlem1ssu  7254  iooval2  9394  hashsng  10267  zfz1isolem1  10306  resqrexlemover  10504  isumclim3  10878  algrp1  11367