Theorem breqtrrid 5162

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  r1sdom  9793  alephordilem1  10092  mulge0  11760  xsubge0  13282  xmulgt0  13304  xmulge0  13305  xlemul1a  13309  sqlecan  14232  bernneq  14252  hashge1  14412  hashge2el2dif  14503  cnpart  15264  sqrt0  15265  bitsfzo  16459  bitsmod  16460  bitsinv1lem  16465  pcge0  16887  prmreclem4  16944  prmreclem5  16945  isnzr2hash  20484  isabvd  20777  abvtrivd  20797  nmolb2d  24662  nmoi  24672  nmoleub  24675  nmo0  24679  ovolge0  25439  itg1ge0a  25669  fta1g  26132  plyrem  26270  taylfval  26323  abelthlem2  26399  sinq12ge0  26474  relogrn  26527  logneg  26554  cxpge0  26649  amgmlem  26957  bposlem5  27256  lgsdir2lem2  27294  2lgsoddprmlem3  27382  rpvmasumlem  27455  mulsge0d  28106  expsgt0  28379  eupth2lem3lem3  30216  eupth2lemb  30223  blocnilem  30790  pjssge0ii  31668  unierri  32090  xlt2addrd  32741  2sqr3minply  33819  locfinref  33877  esumcst  34099  ballotlem5  34537  poimirlem23  37672  poimirlem25  37674  poimirlem26  37675  poimirlem27  37676  poimirlem28  37677  itgaddnclem2  37708  pell14qrgt0  42849  monotoddzzfi  42933  rmxypos  42938  rmygeid  42955  stoweidlem18  46014  stoweidlem55  46051  wallispi2lem1  46067  fourierdlem62  46164  fourierdlem103  46205  fourierdlem104  46206  fourierswlem  46226  2ltceilhalf  47324  ceilhalfnn  47332  pgrpgt2nabl  48308  pw2m1lepw2m1  48463  amgmwlem  49633