Theorem breqtrrid 5113

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

Syntax hints:   → wi 4   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  r1sdom  9693  alephordilem1  9990  mulge0  11663  xsubge0  13208  xmulgt0  13230  xmulge0  13231  xlemul1a  13235  sqlecan  14166  bernneq  14186  hashge1  14346  hashge2el2dif  14437  cnpart  15197  sqrt0  15198  bitsfzo  16399  bitsmod  16400  bitsinv1lem  16405  pcge0  16828  prmreclem4  16885  prmreclem5  16886  isnzr2hash  20495  isabvd  20788  abvtrivd  20808  nmolb2d  24705  nmoi  24715  nmoleub  24718  nmo0  24722  ovolge0  25470  itg1ge0a  25700  fta1g  26157  plyrem  26293  taylfval  26346  abelthlem2  26419  sinq12ge0  26494  relogrn  26547  logneg  26574  cxpge0  26669  amgmlem  26975  bposlem5  27273  lgsdir2lem2  27311  2lgsoddprmlem3  27399  rpvmasumlem  27472  mulsge0d  28160  expsgt0  28451  eupth2lem3lem3  30322  eupth2lemb  30329  blocnilem  30897  pjssge0ii  31775  unierri  32197  xlt2addrd  32855  2sqr3minply  33976  locfinref  34037  esumcst  34259  ballotlem5  34696  poimirlem23  38025  poimirlem25  38027  poimirlem26  38028  poimirlem27  38029  poimirlem28  38030  itgaddnclem2  38061  sn-recgt0d  42982  pell14qrgt0  43319  monotoddzzfi  43402  rmxypos  43407  rmygeid  43424  stoweidlem18  46475  stoweidlem55  46512  wallispi2lem1  46528  fourierdlem62  46625  fourierdlem103  46666  fourierdlem104  46667  fourierswlem  46687  2ltceilhalf  47809  ceilhalfnn  47817  pgrpgt2nabl  48871  pw2m1lepw2m1  49025  amgmwlem  50306