Theorem breqtrrid 5186

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

Hypotheses

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

Assertion

Ref	Expression
breqtrrid	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrid

Step	Hyp	Ref	Expression
1		breqtrrid.1	. 2 ⊢ 𝐴𝑅𝐵
2		breqtrrid.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2738	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	breqtrid 5185	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  r1sdom  9771  alephordilem1  10070  mulge0  11734  xsubge0  13242  xmulgt0  13264  xmulge0  13265  xlemul1a  13269  sqlecan  14175  bernneq  14194  hashge1  14351  hashge2el2dif  14443  cnpart  15189  sqrt0  15190  bitsfzo  16378  bitsmod  16379  bitsinv1lem  16384  pcge0  16797  prmreclem4  16854  prmreclem5  16855  isnzr2hash  20302  isabvd  20432  abvtrivd  20452  nmolb2d  24242  nmoi  24252  nmoleub  24255  nmo0  24259  ovolge0  25005  itg1ge0a  25236  fta1g  25692  plyrem  25825  taylfval  25878  abelthlem2  25951  sinq12ge0  26025  relogrn  26077  logneg  26103  cxpge0  26198  amgmlem  26501  bposlem5  26798  lgsdir2lem2  26836  2lgsoddprmlem3  26924  rpvmasumlem  26997  eupth2lem3lem3  29521  eupth2lemb  29528  blocnilem  30095  pjssge0ii  30973  unierri  31395  xlt2addrd  32009  locfinref  32890  esumcst  33130  ballotlem5  33567  poimirlem23  36597  poimirlem25  36599  poimirlem26  36600  poimirlem27  36601  poimirlem28  36602  itgaddnclem2  36633  pell14qrgt0  41679  monotoddzzfi  41763  rmxypos  41768  rmygeid  41785  stoweidlem18  44813  stoweidlem55  44850  wallispi2lem1  44866  fourierdlem62  44963  fourierdlem103  45004  fourierdlem104  45005  fourierswlem  45025  pgrpgt2nabl  47121  pw2m1lepw2m1  47279  amgmwlem  47927