Theorem breqtrrid 5148

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is used by:  r1sdom  9744  alephordilem1  10064  mulge0  11738  xsubge0  13293  xmulgt0  13315  xmulge0  13316  xlemul1a  13320  sqlecan  14252  bernneq  14272  hashge1  14432  hashge2el2dif  14524  cnpart  15298  sqrt0  15299  bitsfzo  16499  bitsmod  16500  bitsinv1lem  16505  pcge0  16928  prmreclem4  16985  prmreclem5  16986  isnzr2hash  20628  isabvd  20926  abvtrivd  20946  nmolb2d  24886  nmoi  24896  nmoleub  24899  nmo0  24903  ovolge0  25651  itg1ge0a  25881  fta1g  26338  plyrem  26477  taylfval  26533  abelthlem2  26606  sinq12ge0  26684  relogrn  26737  logneg  26764  cxpge0  26859  amgmlem  27165  bposlem5  27463  lgsdir2lem2  27501  2lgsoddprmlem3  27589  rpvmasumlem  27662  mulsge0d  28350  expsgt0  28641  eupth2lem3lem3  30592  eupth2lemb  30599  blocnilem  31167  pjssge0ii  32045  unierri  32467  xlt2addrd  33115  2sqr3minply  34179  locfinref  34240  esumcst  34462  ballotlem5  34899  poimirlem23  38322  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  itgaddnclem2  38358  sn-recgt0d  43279  pell14qrgt0  43614  monotoddzzfi  43697  rmxypos  43702  rmygeid  43719  stoweidlem18  46760  stoweidlem55  46797  wallispi2lem1  46813  fourierdlem62  46910  fourierdlem103  46951  fourierdlem104  46952  fourierswlem  46972  2ltceilhalf  48097  ceilhalfnn  48105  pgrpgt2nabl  49174  pw2m1lepw2m1  49328  amgmwlem  50677