Theorem syl6breqr 2655

Description: A chained equality inference for a binary relation.

Hypotheses

Ref	Expression
syl6breqr.1	|- (ph -> ARB)
syl6breqr.2	|- C = B

Assertion

Ref	Expression
syl6breqr	|- (ph -> ARC)

Proof of Theorem syl6breqr

Step	Hyp	Ref	Expression
1		syl6breqr.1	. 2 |- (ph -> ARB)
2		syl6breqr.2	. . 3 |- C = B
3	2	eqcomi 1479	. 2 |- B = C
4	1, 3	syl6breq 2654	1 |- (ph -> ARC)

Syntax hints:   -> wi 3   = wceq 956   class class class wbr 2619

This theorem is referenced by:  fodomfiOLD 4566  gtndivt 6193  intfrac 6253  intfracOLD 6254  faclbnd4lem1 6948  ser1cmp2lem 7176  infcvglem1 7221  cvgratlem1ALT 7247  ivthlem6 7286  ivthlem7 7287  ivthlem9 7289  eflt 7406  efcnlem1 7419  efcnlem2 7420  sin01bndlem2 7468  cos01bndlem2 7470  infpnlem2 7507  infunabs 7565  infcdaabs 7566  siilem1 8511  minveclem38 8582  pilem2 8672  cosh111lem1 8714  projlem6 9191  pjthlem3 9221  nmopco 10028  stadd 10173

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  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 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620

Copyright terms: Public domain