Theorem breqtrrid 5140

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

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  r1sdom  9703  alephordilem1  10002  mulge0  11672  xsubge0  13197  xmulgt0  13219  xmulge0  13220  xlemul1a  13224  sqlecan  14150  bernneq  14170  hashge1  14330  hashge2el2dif  14421  cnpart  15182  sqrt0  15183  bitsfzo  16381  bitsmod  16382  bitsinv1lem  16387  pcge0  16809  prmreclem4  16866  prmreclem5  16867  isnzr2hash  20439  isabvd  20732  abvtrivd  20752  nmolb2d  24639  nmoi  24649  nmoleub  24652  nmo0  24656  ovolge0  25415  itg1ge0a  25645  fta1g  26108  plyrem  26246  taylfval  26299  abelthlem2  26375  sinq12ge0  26450  relogrn  26503  logneg  26530  cxpge0  26625  amgmlem  26933  bposlem5  27232  lgsdir2lem2  27270  2lgsoddprmlem3  27358  rpvmasumlem  27431  mulsge0d  28089  expsgt0  28364  eupth2lem3lem3  30209  eupth2lemb  30216  blocnilem  30783  pjssge0ii  31661  unierri  32083  xlt2addrd  32732  2sqr3minply  33763  locfinref  33824  esumcst  34046  ballotlem5  34484  poimirlem23  37630  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  poimirlem28  37635  itgaddnclem2  37666  sn-recgt0d  42458  pell14qrgt0  42840  monotoddzzfi  42924  rmxypos  42929  rmygeid  42946  stoweidlem18  46009  stoweidlem55  46046  wallispi2lem1  46062  fourierdlem62  46159  fourierdlem103  46200  fourierdlem104  46201  fourierswlem  46221  2ltceilhalf  47322  ceilhalfnn  47330  pgrpgt2nabl  48347  pw2m1lepw2m1  48502  amgmwlem  49784