Theorem syl5eqr 2186

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

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  3eqtr3g  2195  csbeq1a  3012  ssdifeq0  3445  pofun  4234  opabbi2dv  4688  funimaexg  5207  fresin  5301  f1imacnv  5384  foimacnv  5385  fsn2  5594  fmptpr  5612  funiunfvdm  5664  funiunfvdmf  5665  fcof1o  5690  f1opw2  5976  fnexALT  6011  eqerlem  6460  pmresg  6570  mapsn  6584  fopwdom  6730  mapen  6740  fiintim  6817  xpfi  6818  sbthlemi8  6852  sbthlemi9  6853  ctssdccl  6996  exmidfodomrlemim  7057  mul02  8149  recdivap  8478  fzpreddisj  9851  fzshftral  9888  qbtwnrelemcalc  10033  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  binom3  10409  bcn2  10510  hashfz1  10529  hashunlem  10550  hashfacen  10579  cnrecnv  10682  resqrexlemnm  10790  amgm2  10890  2zsupmax  10997  xrmaxltsup  11027  xrmaxadd  11030  xrbdtri  11045  fisumss  11161  fsumcnv  11206  telfsumo  11235  fsumiun  11246  arisum2  11268  ege2le3  11377  efgt1p  11402  cos01bnd  11465  dfgcd3  11698  eucalgval  11735  sqrt2irrlem  11839  setsslid  12009  baspartn  12217  txdis1cn  12447  cnmpt21  12460  cnmpt22  12463  hmeores  12484  metreslem  12549  remetdval  12708  dvfvalap  12819  nninfsellemqall  13211