Theorem breqtrrid 5142

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  r1sdom  9781  alephordilem1  10152  mulge0  11834  xsubge0  13391  xmulgt0  13413  xmulge0  13414  xlemul1a  13418  sqlecan  14353  bernneq  14373  hashge1  14533  hashge2el2dif  14625  cnpart  15407  sqrt0  15408  bitsfzo  16605  bitsmod  16606  bitsinv1lem  16611  pcge0  17040  prmreclem4  17097  prmreclem5  17098  isnzr2hash  20770  isabvd  21069  abvtrivd  21089  nmolb2d  25037  nmoi  25047  nmoleub  25050  nmo0  25054  ovolge0  25802  itg1ge0a  26032  fta1g  26488  plyrem  26626  taylfval  26686  abelthlem2  26759  sinq12ge0  26837  relogrn  26889  logneg  26916  cxpge0  27011  amgmlem  27317  bposlem5  27615  lgsdir2lem2  27653  2lgsoddprmlem3  27741  rpvmasumlem  27814  mulsge0d  28532  expsgt0  28823  eupth2lem3lem3  30831  eupth2lemb  30838  blocnilem  31406  pjssge0ii  32284  unierri  32706  xlt2addrd  33351  2sqr3minply  34412  locfinref  34473  esumcst  34695  ballotlem5  35132  poimirlem23  38562  poimirlem25  38564  poimirlem26  38565  poimirlem27  38566  poimirlem28  38567  itgaddnclem2  38598  sn-recgt0d  43542  pell14qrgt0  43866  monotoddzzfi  43949  rmxypos  43954  rmygeid  43971  stoweidlem18  47028  stoweidlem55  47065  wallispi2lem1  47081  fourierdlem62  47178  fourierdlem103  47219  fourierdlem104  47220  fourierswlem  47240  2ltceilhalf  48402  ceilhalfnn  48410  pgrpgt2nabl  49478  pw2m1lepw2m1  49632  amgmwlem  50987