Theorem breqtrrid 5181

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  r1sdom  9814  alephordilem1  10113  mulge0  11781  xsubge0  13303  xmulgt0  13325  xmulge0  13326  xlemul1a  13330  sqlecan  14248  bernneq  14268  hashge1  14428  hashge2el2dif  14519  cnpart  15279  sqrt0  15280  bitsfzo  16472  bitsmod  16473  bitsinv1lem  16478  pcge0  16900  prmreclem4  16957  prmreclem5  16958  isnzr2hash  20519  isabvd  20813  abvtrivd  20833  nmolb2d  24739  nmoi  24749  nmoleub  24752  nmo0  24756  ovolge0  25516  itg1ge0a  25746  fta1g  26209  plyrem  26347  taylfval  26400  abelthlem2  26476  sinq12ge0  26550  relogrn  26603  logneg  26630  cxpge0  26725  amgmlem  27033  bposlem5  27332  lgsdir2lem2  27370  2lgsoddprmlem3  27458  rpvmasumlem  27531  mulsge0d  28172  expsgt0  28415  eupth2lem3lem3  30249  eupth2lemb  30256  blocnilem  30823  pjssge0ii  31701  unierri  32123  xlt2addrd  32762  2sqr3minply  33791  locfinref  33840  esumcst  34064  ballotlem5  34502  poimirlem23  37650  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  itgaddnclem2  37686  pell14qrgt0  42870  monotoddzzfi  42954  rmxypos  42959  rmygeid  42976  stoweidlem18  46033  stoweidlem55  46070  wallispi2lem1  46086  fourierdlem62  46183  fourierdlem103  46224  fourierdlem104  46225  fourierswlem  46245  2ltceilhalf  48015  pgrpgt2nabl  48282  pw2m1lepw2m1  48437  amgmwlem  49321