Theorem breqtrrdi 4046

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 2181	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtrdi 4045	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 4004

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005

This theorem is referenced by:  enpr2d  6817  fiunsnnn  6881  unsnfi  6918  eninl  7096  eninr  7097  difinfinf  7100  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  dju1en  7212  djucomen  7215  djuassen  7216  xpdjuen  7217  gtndiv  9348  intqfrac2  10319  uzenom  10425  xrmaxiflemval  11258  ege2le3  11679  eirraplem  11784  pcprendvds  12290  pcpremul  12293  pcfaclem  12347  infpnlem2  12358  2strstr1g  12580  lmcn2  13783  dveflem  14190  tangtx  14262  ioocosf1o  14278  lgsdirprm  14438  sbthom  14777  nconstwlpolemgt0  14814