Theorem breqtrrid 5135

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

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

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 2707

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 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  r1sdom  9688  alephordilem1  9985  mulge0  11657  xsubge0  13178  xmulgt0  13200  xmulge0  13201  xlemul1a  13205  sqlecan  14134  bernneq  14154  hashge1  14314  hashge2el2dif  14405  cnpart  15165  sqrt0  15166  bitsfzo  16364  bitsmod  16365  bitsinv1lem  16370  pcge0  16792  prmreclem4  16849  prmreclem5  16850  isnzr2hash  20454  isabvd  20747  abvtrivd  20767  nmolb2d  24664  nmoi  24674  nmoleub  24677  nmo0  24681  ovolge0  25440  itg1ge0a  25670  fta1g  26133  plyrem  26271  taylfval  26324  abelthlem2  26400  sinq12ge0  26475  relogrn  26528  logneg  26555  cxpge0  26650  amgmlem  26958  bposlem5  27257  lgsdir2lem2  27295  2lgsoddprmlem3  27383  rpvmasumlem  27456  mulsge0d  28126  expsgt0  28414  eupth2lem3lem3  30286  eupth2lemb  30293  blocnilem  30860  pjssge0ii  31738  unierri  32160  xlt2addrd  32818  2sqr3minply  33916  locfinref  33977  esumcst  34199  ballotlem5  34636  poimirlem23  37813  poimirlem25  37815  poimirlem26  37816  poimirlem27  37817  poimirlem28  37818  itgaddnclem2  37849  sn-recgt0d  42769  pell14qrgt0  43138  monotoddzzfi  43221  rmxypos  43226  rmygeid  43243  stoweidlem18  46299  stoweidlem55  46336  wallispi2lem1  46352  fourierdlem62  46449  fourierdlem103  46490  fourierdlem104  46491  fourierswlem  46511  2ltceilhalf  47611  ceilhalfnn  47619  pgrpgt2nabl  48649  pw2m1lepw2m1  48803  amgmwlem  50084