Theorem syl5eqr 2127

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

Hypotheses

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

Assertion

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

Proof of Theorem syl5eqr

Step	Hyp	Ref	Expression
1		syl5eqr.1	. . 3 |- B = A
2	1	eqcomi 2085	. 2 |- A = B
3		syl5eqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5eq 2125	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  3eqtr3g  2136  csbeq1a  2916  ssdifeq0  3325  pofun  4067  opabbi2dv  4503  funimaexg  5003  fresin  5088  f1imacnv  5163  foimacnv  5164  fsn2  5358  fmptpr  5376  funiunfvdm  5423  funiunfvdmf  5424  fcof1o  5449  f1opw2  5726  fnexALT  5760  eqerlem  6160  fopwdom  6333  mul02  7491  recdivap  7806  fzpreddisj  9088  fzshftral  9125  qbtwnrelemcalc  9264  frec2uzrdg  9411  binom3  9590  bcn2  9691  cnrecnv  9797  resqrexlemnm  9904  amgm2  10004  dfgcd3  10399  eucalgval  10436  sqrt2irrlem  10540