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

Syntax hints:   → wi 4   = wceq 1540   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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  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  9773  alephordilem1  10072  mulge0  11737  xsubge0  13245  xmulgt0  13267  xmulge0  13268  xlemul1a  13272  sqlecan  14178  bernneq  14197  hashge1  14354  hashge2el2dif  14446  cnpart  15192  sqrt0  15193  bitsfzo  16381  bitsmod  16382  bitsinv1lem  16387  pcge0  16800  prmreclem4  16857  prmreclem5  16858  isnzr2hash  20411  isabvd  20572  abvtrivd  20592  nmolb2d  24456  nmoi  24466  nmoleub  24469  nmo0  24473  ovolge0  25231  itg1ge0a  25462  fta1g  25921  plyrem  26055  taylfval  26108  abelthlem2  26181  sinq12ge0  26255  relogrn  26307  logneg  26333  cxpge0  26428  amgmlem  26731  bposlem5  27028  lgsdir2lem2  27066  2lgsoddprmlem3  27154  rpvmasumlem  27227  eupth2lem3lem3  29751  eupth2lemb  29758  blocnilem  30325  pjssge0ii  31203  unierri  31625  xlt2addrd  32239  locfinref  33120  esumcst  33360  ballotlem5  33797  poimirlem23  36815  poimirlem25  36817  poimirlem26  36818  poimirlem27  36819  poimirlem28  36820  itgaddnclem2  36851  pell14qrgt0  41900  monotoddzzfi  41984  rmxypos  41989  rmygeid  42006  stoweidlem18  45033  stoweidlem55  45070  wallispi2lem1  45086  fourierdlem62  45183  fourierdlem103  45224  fourierdlem104  45225  fourierswlem  45245  pgrpgt2nabl  47131  pw2m1lepw2m1  47289  amgmwlem  47937