Theorem syl5breqr 4723

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

Hypotheses

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

Assertion

Ref	Expression
syl5breqr	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem syl5breqr

Step	Hyp	Ref	Expression
1		syl5breqr.1	. 2 ⊢ 𝐴𝑅𝐵
2		syl5breqr.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2657	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	syl5breq 4722	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1523   class class class wbr 4685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686

This theorem is referenced by:  r1sdom  8675  alephordilem1  8934  mulge0  10584  xsubge0  12129  xmulgt0  12151  xmulge0  12152  xlemul1a  12156  sqlecan  13011  bernneq  13030  hashge1  13216  hashge2el2dif  13300  cnpart  14024  sqr0lem  14025  bitsfzo  15204  bitsmod  15205  bitsinv1lem  15210  pcge0  15613  prmreclem4  15670  prmreclem5  15671  isabvd  18868  abvtrivd  18888  isnzr2hash  19312  nmolb2d  22569  nmoi  22579  nmoleub  22582  nmo0  22586  ovolge0  23295  itg1ge0a  23523  fta1g  23972  plyrem  24105  taylfval  24158  abelthlem2  24231  sinq12ge0  24305  relogrn  24353  logneg  24379  cxpge0  24474  amgmlem  24761  bposlem5  25058  lgsdir2lem2  25096  2lgsoddprmlem3  25184  rpvmasumlem  25221  eupth2lem3lem3  27208  eupth2lemb  27215  blocnilem  27787  pjssge0ii  28669  unierri  29091  xlt2addrd  29651  locfinref  30036  esumcst  30253  ballotlem5  30689  poimirlem23  33562  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  itgaddnclem2  33599  pell14qrgt0  37740  monotoddzzfi  37824  rmxypos  37831  rmygeid  37848  stoweidlem18  40553  stoweidlem55  40590  wallispi2lem1  40606  fourierdlem62  40703  fourierdlem103  40744  fourierdlem104  40745  fourierswlem  40765  pgrpgt2nabl  42472  pw2m1lepw2m1  42635  amgmwlem  42876