Theorem breqtrdi 4130

Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)

Hypotheses

Ref	Expression
breqtrdi.1	|- ( ph -> A R B )
breqtrdi.2	|- B = C

Assertion

Ref	Expression
breqtrdi	|- ( ph -> A R C )

Proof of Theorem breqtrdi

Step	Hyp	Ref	Expression
1		breqtrdi.1	. 2 |- ( ph -> A R B )
2		eqid 2230	. 2 |- A = A
3		breqtrdi.2	. 2 |- B = C
4	1, 2, 3	3brtr3g 4122	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1397   class class class wbr 4089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-un 3203  df-sn 3676  df-pr 3677  df-op 3679  df-br 4090

This theorem is referenced by:  breqtrrdi  4131  en2eleq  7411  en2other2  7412  dju0en  7434  ltm1sr  8002  maxle2  11795  xrmax2sup  11837  mertenslem2  12120  ege2le3  12255  cos01gt0  12347  sin02gt0  12348  cos12dec  12352  bitsfzolem  12538  bitsmod  12540  unennn  13041  dvef  15480  sin0pilem2  15535  cosq23lt0  15586  cosq34lt1  15603  cos02pilt1  15604  logbgcd1irraplemexp  15721  lgslem3  15760  lgsquadlem1  15835  lgsquadlem3  15837  trilpolemeq1  16711