Theorem syl5breqr 4961

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

Syntax hints:   → wi 4   = wceq 1507   class class class wbr 4923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924

This theorem is referenced by:  r1sdom  8989  alephordilem1  9285  mulge0  10951  xsubge0  12463  xmulgt0  12485  xmulge0  12486  xlemul1a  12490  sqlecan  13379  bernneq  13398  hashge1  13556  hashge2el2dif  13639  cnpart  14450  sqr0lem  14451  bitsfzo  15634  bitsmod  15635  bitsinv1lem  15640  pcge0  16044  prmreclem4  16101  prmreclem5  16102  isabvd  19303  abvtrivd  19323  isnzr2hash  19748  nmolb2d  23020  nmoi  23030  nmoleub  23033  nmo0  23037  ovolge0  23775  itg1ge0a  24005  fta1g  24454  plyrem  24587  taylfval  24640  abelthlem2  24713  sinq12ge0  24787  relogrn  24836  logneg  24862  cxpge0  24957  amgmlem  25259  bposlem5  25556  lgsdir2lem2  25594  2lgsoddprmlem3  25682  rpvmasumlem  25755  eupth2lem3lem3  27750  eupth2lemb  27757  blocnilem  28348  pjssge0ii  29230  unierri  29652  xlt2addrd  30223  locfinref  30706  esumcst  30923  ballotlem5  31360  poimirlem23  34304  poimirlem25  34306  poimirlem26  34307  poimirlem27  34308  poimirlem28  34309  itgaddnclem2  34340  pell14qrgt0  38797  monotoddzzfi  38880  rmxypos  38885  rmygeid  38902  stoweidlem18  41680  stoweidlem55  41717  wallispi2lem1  41733  fourierdlem62  41830  fourierdlem103  41871  fourierdlem104  41872  fourierswlem  41892  pgrpgt2nabl  43720  pw2m1lepw2m1  43883  amgmwlem  44210