Theorem syl6breq 2644

Description: A chained equality inference for a binary relation.

Hypotheses

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

Assertion

Ref	Expression
syl6breq	|- (ph -> ARC)

Proof of Theorem syl6breq

Step	Hyp	Ref	Expression
1		syl6breq.1	. 2 |- (ph -> ARB)
2		eqid 1468	. 2 |- A = A
3		syl6breq.2	. 2 |- B = C
4	1, 2, 3	3brtr3g 2636	1 |- (ph -> ARC)

Syntax hints:   -> wi 3   = wceq 953   class class class wbr 2609

This theorem is referenced by:  syl6breqr 2645  ltbtwnpq 5056  1pr 5089  prlem934 5111  ltexprlem2 5115  msqgt0 5587  recgt0i 5770  zltp1let 6128  exple1t 6538  abs3lem 6838  faclbnd4lem1 6885  isumclim3t 7135  ivthlem1 7216  ivthlem6 7221  ivthlem6OLD 7230  efcvg 7256  cos01gt0 7419  sin02gt0 7420  infcda 7510  infxp 7515  alephadd 7524  minveclem30 8505  norm3lem 8937  projlem12 9113  nmopadjlem 9937  nmopcoadj 9948  hstlet 10067  stadd3 10085  strlem3a 10089  strlem5 10092

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610

Copyright terms: Public domain