Theorem syl6breqr 2660

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 1482	. 2 |- B = C
4	1, 3	syl6breq 2659	1 |- (ph -> ARC)

Syntax hints:   -> wi 3   = wceq 958   class class class wbr 2624

This theorem is referenced by:  fodomfi 4575  fodomfiOLD 4576  gtndivt 6195  intfrac 6254  faclbnd4lem1 6948  ser1cmp2lem 7176  infcvglem1 7221  cvgratlem1ALT 7247  ivthlem6 7286  ivthlem7 7287  ivthlem9 7289  eflt 7406  efcnlem1 7419  efcnlem2 7420  sin01bndlem2 7469  cos01bndlem2 7471  infpnlem2 7508  infunabs 7566  infcdaabs 7567  siilem1 8507  minveclem38 8578  pilem2 8667  cosh111lem1 8709  projlem6 9186  pjthlem3 9216  nmopco 10023  stadd 10168

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053  df-sn 2416  df-pr 2417  df-op 2420  df-br 2625

Copyright terms: Public domain