Theorem syl5eqbr 2645

Description: A chained equality inference for a binary relation.

Hypotheses

Ref	Expression
syl5eqbr.1	|- (ph -> ARB)
syl5eqbr.2	|- C = A

Assertion

Ref	Expression
syl5eqbr	|- (ph -> CRB)

Proof of Theorem syl5eqbr

Step	Hyp	Ref	Expression
1		syl5eqbr.1	. 2 |- (ph -> ARB)
2		syl5eqbr.2	. 2 |- C = A
3		eqid 1475	. 2 |- B = B
4	1, 2, 3	3brtr4g 2644	1 |- (ph -> CRB)

Syntax hints:   -> wi 3   = wceq 955   class class class wbr 2616

This theorem is referenced by:  imadomg 4793  iundom 4799  sucxpdom 4833  cdaun 4909  supxrmnf 6048  nn0ltp1let 6088  bernneq2 6603  faclbnd4lem1 6914  isumclim3t 7171  infcvgaux2 7191  geolim 7208  geolim1 7210  ivthlem6 7257  ivthlem7 7258  ivthlem7OLD 7267  efcvg 7292  efaddlem15 7330  efaddlem23 7338  effsumle 7374  efge1 7378  efge1p 7379  efcnlem2 7396  unictb 7555  cctop 7631  blocnilem 8448  minveclem38 8566  minvecle 8570  strlem5 10173  hstrlem5 10181

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1810  df-un 2048  df-sn 2410  df-pr 2411  df-op 2414  df-br 2617

Copyright terms: Public domain