Theorem breqtrdi 4062

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 2189	. 2 |- A = A
3		breqtrdi.2	. 2 |- B = C
4	1, 2, 3	3brtr3g 4054	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4021

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3616  df-pr 3617  df-op 3619  df-br 4022

This theorem is referenced by:  breqtrrdi  4063  en2eleq  7229  en2other2  7230  dju0en  7248  ltm1sr  7811  maxle2  11262  xrmax2sup  11303  mertenslem2  11585  ege2le3  11720  cos01gt0  11811  sin02gt0  11812  cos12dec  11816  unennn  12459  dvef  14673  sin0pilem2  14688  cosq23lt0  14739  cosq34lt1  14756  cos02pilt1  14757  logbgcd1irraplemexp  14871  lgslem3  14889  trilpolemeq1  15276