Theorem breqtrrid 5157

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

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

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 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  r1sdom  9786  alephordilem1  10085  mulge0  11753  xsubge0  13275  xmulgt0  13297  xmulge0  13298  xlemul1a  13302  sqlecan  14225  bernneq  14245  hashge1  14405  hashge2el2dif  14496  cnpart  15257  sqrt0  15258  bitsfzo  16452  bitsmod  16453  bitsinv1lem  16458  pcge0  16880  prmreclem4  16937  prmreclem5  16938  isnzr2hash  20477  isabvd  20770  abvtrivd  20790  nmolb2d  24655  nmoi  24665  nmoleub  24668  nmo0  24672  ovolge0  25432  itg1ge0a  25662  fta1g  26125  plyrem  26263  taylfval  26316  abelthlem2  26392  sinq12ge0  26467  relogrn  26520  logneg  26547  cxpge0  26642  amgmlem  26950  bposlem5  27249  lgsdir2lem2  27287  2lgsoddprmlem3  27375  rpvmasumlem  27448  mulsge0d  28089  expsgt0  28332  eupth2lem3lem3  30157  eupth2lemb  30164  blocnilem  30731  pjssge0ii  31609  unierri  32031  xlt2addrd  32682  2sqr3minply  33760  locfinref  33818  esumcst  34040  ballotlem5  34478  poimirlem23  37613  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  itgaddnclem2  37649  pell14qrgt0  42829  monotoddzzfi  42913  rmxypos  42918  rmygeid  42935  stoweidlem18  45995  stoweidlem55  46032  wallispi2lem1  46048  fourierdlem62  46145  fourierdlem103  46186  fourierdlem104  46187  fourierswlem  46207  2ltceilhalf  47305  ceilhalfnn  47313  pgrpgt2nabl  48289  pw2m1lepw2m1  48444  amgmwlem  49614