Theorem syl5breqr 4621

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

Syntax hints:   → wi 4   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  r1sdom  8520  alephordilem1  8779  mulge0  10425  xsubge0  11963  xmulgt0  11985  xmulge0  11986  xlemul1a  11990  sqlecan  12833  bernneq  12852  hashge1  13039  hashge2el2dif  13117  cnpart  13828  sqr0lem  13829  bitsfzo  14995  bitsmod  14996  bitsinv1lem  15001  pcge0  15404  prmreclem4  15461  prmreclem5  15462  isabvd  18643  abvtrivd  18663  isnzr2hash  19085  nmolb2d  22332  nmoi  22342  nmoleub  22345  nmo0  22349  ovolge0  23056  itg1ge0a  23284  fta1g  23731  plyrem  23864  taylfval  23917  abelthlem2  23990  sinq12ge0  24064  relogrn  24112  logneg  24138  cxpge0  24229  amgmlem  24516  bposlem5  24813  lgsdir2lem2  24851  2lgsoddprmlem3  24939  rpvmasumlem  24976  eupath2lem3  26506  eupath2  26507  frgrawopreglem2  26572  blocnilem  27043  pjssge0ii  27925  unierri  28347  xlt2addrd  28913  locfinref  29236  esumcst  29452  ballotlem5  29888  poimirlem23  32602  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  itgaddnclem2  32639  pell14qrgt0  36441  monotoddzzfi  36525  rmxypos  36532  rmygeid  36549  stoweidlem18  38911  stoweidlem55  38948  wallispi2lem1  38964  fourierdlem62  39061  fourierdlem103  39102  fourierdlem104  39103  fourierswlem  39123  eupth2lem3lem3  41398  eupth2lemb  41405  pgrpgt2nabl  41941  pw2m1lepw2m1  42104  amgmwlem  42357