Theorem syl5eqr 2135

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 2093	. 2 |- A = B
3		syl5eqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5eq 2133	1 |- ( ph -> A = C )

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:  3eqtr3g  2144  csbeq1a  2942  ssdifeq0  3369  pofun  4148  opabbi2dv  4598  funimaexg  5111  fresin  5202  f1imacnv  5283  foimacnv  5284  fsn2  5485  fmptpr  5503  funiunfvdm  5556  funiunfvdmf  5557  fcof1o  5582  f1opw2  5864  fnexALT  5898  eqerlem  6337  pmresg  6447  mapsn  6461  fopwdom  6606  mapen  6616  fiintim  6693  xpfi  6694  sbthlemi8  6727  sbthlemi9  6728  exmidfodomrlemim  6888  mul02  7926  recdivap  8246  fzpreddisj  9546  fzshftral  9583  qbtwnrelemcalc  9728  frec2uzrdg  9877  frecuzrdgrcl  9878  frecuzrdgsuc  9882  frecuzrdgrclt  9883  frecuzrdgg  9884  binom3  10132  bcn2  10233  hashfz1  10252  hashunlem  10273  hashfacen  10302  cnrecnv  10405  resqrexlemnm  10512  amgm2  10612  2zsupmax  10718  fisumss  10845  fsumcnv  10892  telfsumo  10921  fsumiun  10932  arisum2  10954  ege2le3  11022  efgt1p  11047  cos01bnd  11110  dfgcd3  11338  eucalgval  11375  sqrt2irrlem  11479  setsslid  11605  baspartn  11809  nninfsellemqall  12179