Theorem breqtrrid 5130

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  r1sdom  9670  alephordilem1  9967  mulge0  11638  xsubge0  13163  xmulgt0  13185  xmulge0  13186  xlemul1a  13190  sqlecan  14116  bernneq  14136  hashge1  14296  hashge2el2dif  14387  cnpart  15147  sqrt0  15148  bitsfzo  16346  bitsmod  16347  bitsinv1lem  16352  pcge0  16774  prmreclem4  16831  prmreclem5  16832  isnzr2hash  20404  isabvd  20697  abvtrivd  20717  nmolb2d  24604  nmoi  24614  nmoleub  24617  nmo0  24621  ovolge0  25380  itg1ge0a  25610  fta1g  26073  plyrem  26211  taylfval  26264  abelthlem2  26340  sinq12ge0  26415  relogrn  26468  logneg  26495  cxpge0  26590  amgmlem  26898  bposlem5  27197  lgsdir2lem2  27235  2lgsoddprmlem3  27323  rpvmasumlem  27396  mulsge0d  28056  expsgt0  28331  eupth2lem3lem3  30178  eupth2lemb  30185  blocnilem  30752  pjssge0ii  31630  unierri  32052  xlt2addrd  32711  2sqr3minply  33763  locfinref  33824  esumcst  34046  ballotlem5  34484  poimirlem23  37643  poimirlem25  37645  poimirlem26  37646  poimirlem27  37647  poimirlem28  37648  itgaddnclem2  37679  sn-recgt0d  42470  pell14qrgt0  42852  monotoddzzfi  42935  rmxypos  42940  rmygeid  42957  stoweidlem18  46019  stoweidlem55  46056  wallispi2lem1  46072  fourierdlem62  46169  fourierdlem103  46210  fourierdlem104  46211  fourierswlem  46231  2ltceilhalf  47332  ceilhalfnn  47340  pgrpgt2nabl  48370  pw2m1lepw2m1  48525  amgmwlem  49807