Theorem breqtrrid 5112

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5074

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075

This theorem is referenced by:  r1sdom  9532  alephordilem1  9829  mulge0  11493  xsubge0  12995  xmulgt0  13017  xmulge0  13018  xlemul1a  13022  sqlecan  13925  bernneq  13944  hashge1  14104  hashge2el2dif  14194  cnpart  14951  sqr0lem  14952  bitsfzo  16142  bitsmod  16143  bitsinv1lem  16148  pcge0  16563  prmreclem4  16620  prmreclem5  16621  isabvd  20080  abvtrivd  20100  isnzr2hash  20535  nmolb2d  23882  nmoi  23892  nmoleub  23895  nmo0  23899  ovolge0  24645  itg1ge0a  24876  fta1g  25332  plyrem  25465  taylfval  25518  abelthlem2  25591  sinq12ge0  25665  relogrn  25717  logneg  25743  cxpge0  25838  amgmlem  26139  bposlem5  26436  lgsdir2lem2  26474  2lgsoddprmlem3  26562  rpvmasumlem  26635  eupth2lem3lem3  28594  eupth2lemb  28601  blocnilem  29166  pjssge0ii  30044  unierri  30466  xlt2addrd  31081  locfinref  31791  esumcst  32031  ballotlem5  32466  poimirlem23  35800  poimirlem25  35802  poimirlem26  35803  poimirlem27  35804  poimirlem28  35805  itgaddnclem2  35836  pell14qrgt0  40681  monotoddzzfi  40764  rmxypos  40769  rmygeid  40786  stoweidlem18  43559  stoweidlem55  43596  wallispi2lem1  43612  fourierdlem62  43709  fourierdlem103  43750  fourierdlem104  43751  fourierswlem  43771  pgrpgt2nabl  45702  pw2m1lepw2m1  45861  amgmwlem  46506