Theorem syl5breqr 4615

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

Syntax hints:   → wi 4   = wceq 1474   class class class wbr 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578

This theorem is referenced by:  r1sdom  8498  alephordilem1  8757  mulge0  10398  xsubge0  11923  xmulgt0  11945  xmulge0  11946  xlemul1a  11950  sqlecan  12791  bernneq  12810  hashge1  12994  hashge2el2dif  13070  cnpart  13777  sqr0lem  13778  bitsfzo  14944  bitsmod  14945  bitsinv1lem  14950  pcge0  15353  prmreclem4  15410  prmreclem5  15411  isabvd  18592  abvtrivd  18612  isnzr2hash  19034  nmolb2d  22280  nmoi  22290  nmoleub  22293  nmo0  22297  ovolge0  23001  itg1ge0a  23229  fta1g  23676  plyrem  23809  taylfval  23862  abelthlem2  23935  sinq12ge0  24009  relogrn  24057  logneg  24083  cxpge0  24174  amgmlem  24461  bposlem5  24758  lgsdir2lem2  24796  2lgsoddprmlem3  24884  rpvmasumlem  24921  eupath2lem3  26300  eupath2  26301  frgrawopreglem2  26366  blocnilem  26877  pjssge0ii  27759  unierri  28181  xlt2addrd  28747  locfinref  29070  esumcst  29286  ballotlem5  29722  poimirlem23  32426  poimirlem25  32428  poimirlem26  32429  poimirlem27  32430  poimirlem28  32431  itgaddnclem2  32463  pell14qrgt0  36265  monotoddzzfi  36349  rmxypos  36356  rmygeid  36373  stoweidlem18  38735  stoweidlem55  38772  wallispi2lem1  38788  fourierdlem62  38885  fourierdlem103  38926  fourierdlem104  38927  fourierswlem  38947  eupth2lem3lem3  41420  eupth2lemb  41427  pgrpgt2nabl  41963  pw2m1lepw2m1  42126  amgmwlem  42340