Theorem breqtrrdi 4023

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

Hypotheses

Ref	Expression
breqtrrdi.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrrdi.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
breqtrrdi	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrdi

Step	Hyp	Ref	Expression
1		breqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2169	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtrdi 4022	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1343   class class class wbr 3981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-br 3982

This theorem is referenced by:  enpr2d  6779  fiunsnnn  6843  unsnfi  6880  eninl  7058  eninr  7059  difinfinf  7062  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  dju1en  7165  djucomen  7168  djuassen  7169  xpdjuen  7170  gtndiv  9282  intqfrac2  10250  uzenom  10356  xrmaxiflemval  11187  ege2le3  11608  eirraplem  11713  pcprendvds  12218  pcpremul  12221  pcfaclem  12275  infpnlem2  12286  2strstr1g  12493  lmcn2  12880  dveflem  13287  tangtx  13359  ioocosf1o  13375  lgsdirprm  13535  sbthom  13865  nconstwlpolemgt0  13902