Theorem breqtrrid 5137

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5099

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  r1sdom  9690  alephordilem1  9987  mulge0  11659  xsubge0  13180  xmulgt0  13202  xmulge0  13203  xlemul1a  13207  sqlecan  14136  bernneq  14156  hashge1  14316  hashge2el2dif  14407  cnpart  15167  sqrt0  15168  bitsfzo  16366  bitsmod  16367  bitsinv1lem  16372  pcge0  16794  prmreclem4  16851  prmreclem5  16852  isnzr2hash  20456  isabvd  20749  abvtrivd  20769  nmolb2d  24666  nmoi  24676  nmoleub  24679  nmo0  24683  ovolge0  25442  itg1ge0a  25672  fta1g  26135  plyrem  26273  taylfval  26326  abelthlem2  26402  sinq12ge0  26477  relogrn  26530  logneg  26557  cxpge0  26652  amgmlem  26960  bposlem5  27259  lgsdir2lem2  27297  2lgsoddprmlem3  27385  rpvmasumlem  27458  mulsge0d  28146  expsgt0  28437  eupth2lem3lem3  30309  eupth2lemb  30316  blocnilem  30883  pjssge0ii  31761  unierri  32183  xlt2addrd  32841  2sqr3minply  33939  locfinref  34000  esumcst  34222  ballotlem5  34659  poimirlem23  37846  poimirlem25  37848  poimirlem26  37849  poimirlem27  37850  poimirlem28  37851  itgaddnclem2  37882  sn-recgt0d  42799  pell14qrgt0  43168  monotoddzzfi  43251  rmxypos  43256  rmygeid  43273  stoweidlem18  46329  stoweidlem55  46366  wallispi2lem1  46382  fourierdlem62  46479  fourierdlem103  46520  fourierdlem104  46521  fourierswlem  46541  2ltceilhalf  47641  ceilhalfnn  47649  pgrpgt2nabl  48679  pw2m1lepw2m1  48833  amgmwlem  50114