Theorem breqtrrid 5108

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 5107	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  r1sdom  9463  alephordilem1  9760  mulge0  11423  xsubge0  12924  xmulgt0  12946  xmulge0  12947  xlemul1a  12951  sqlecan  13853  bernneq  13872  hashge1  14032  hashge2el2dif  14122  cnpart  14879  sqr0lem  14880  bitsfzo  16070  bitsmod  16071  bitsinv1lem  16076  pcge0  16491  prmreclem4  16548  prmreclem5  16549  isabvd  19995  abvtrivd  20015  isnzr2hash  20448  nmolb2d  23788  nmoi  23798  nmoleub  23801  nmo0  23805  ovolge0  24550  itg1ge0a  24781  fta1g  25237  plyrem  25370  taylfval  25423  abelthlem2  25496  sinq12ge0  25570  relogrn  25622  logneg  25648  cxpge0  25743  amgmlem  26044  bposlem5  26341  lgsdir2lem2  26379  2lgsoddprmlem3  26467  rpvmasumlem  26540  eupth2lem3lem3  28495  eupth2lemb  28502  blocnilem  29067  pjssge0ii  29945  unierri  30367  xlt2addrd  30983  locfinref  31693  esumcst  31931  ballotlem5  32366  poimirlem23  35727  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  itgaddnclem2  35763  pell14qrgt0  40597  monotoddzzfi  40680  rmxypos  40685  rmygeid  40702  stoweidlem18  43449  stoweidlem55  43486  wallispi2lem1  43502  fourierdlem62  43599  fourierdlem103  43640  fourierdlem104  43641  fourierswlem  43661  pgrpgt2nabl  45590  pw2m1lepw2m1  45749  amgmwlem  46392