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  9775  alephordilem1  10074  mulge0  11739  xsubge0  13247  xmulgt0  13269  xmulge0  13270  xlemul1a  13274  sqlecan  14180  bernneq  14199  hashge1  14356  hashge2el2dif  14448  cnpart  15194  sqrt0  15195  bitsfzo  16383  bitsmod  16384  bitsinv1lem  16389  pcge0  16802  prmreclem4  16859  prmreclem5  16860  isnzr2hash  20414  isabvd  20575  abvtrivd  20595  nmolb2d  24468  nmoi  24478  nmoleub  24481  nmo0  24485  ovolge0  25243  itg1ge0a  25474  fta1g  25934  plyrem  26068  taylfval  26121  abelthlem2  26195  sinq12ge0  26269  relogrn  26321  logneg  26347  cxpge0  26442  amgmlem  26745  bposlem5  27042  lgsdir2lem2  27080  2lgsoddprmlem3  27168  rpvmasumlem  27241  eupth2lem3lem3  29765  eupth2lemb  29772  blocnilem  30339  pjssge0ii  31217  unierri  31639  xlt2addrd  32253  locfinref  33134  esumcst  33374  ballotlem5  33811  poimirlem23  36827  poimirlem25  36829  poimirlem26  36830  poimirlem27  36831  poimirlem28  36832  itgaddnclem2  36863  pell14qrgt0  41912  monotoddzzfi  41996  rmxypos  42001  rmygeid  42018  stoweidlem18  45045  stoweidlem55  45082  wallispi2lem1  45098  fourierdlem62  45195  fourierdlem103  45236  fourierdlem104  45237  fourierswlem  45257  pgrpgt2nabl  47143  pw2m1lepw2m1  47301  amgmwlem  47949