Theorem breqtrrdi 4131

Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)

Hypotheses

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

Assertion

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

Proof of Theorem breqtrrdi

Step	Hyp	Ref	Expression
1		breqtrrdi.1	. 2 |- ( ph -> A R B )
2		breqtrrdi.2	. . 3 |- C = B
3	2	eqcomi 2234	. 2 |- B = C
4	1, 3	breqtrdi 4130	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:  enpr2d  7002  fiunsnnn  7075  exmidpw2en  7109  unsnfi  7116  eninl  7301  eninr  7302  difinfinf  7305  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  dju1en  7433  djucomen  7436  djuassen  7437  xpdjuen  7438  gtndiv  9580  intqfrac2  10587  uzenom  10693  xrmaxiflemval  11833  ege2le3  12255  eirraplem  12361  bitsfzo  12539  pcprendvds  12886  pcpremul  12889  pcfaclem  12945  infpnlem2  12956  2strstr1g  13228  lmcn2  15033  dveflem  15479  tangtx  15591  ioocosf1o  15607  lgsdirprm  15792  sbthom  16693  nconstwlpolemgt0  16736