Theorem breqtrrid 5070

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

Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3863  df-sn 4523  df-pr 4525  df-op 4529  df-br 5033

This theorem is referenced by:  r1sdom  9236  alephordilem1  9533  mulge0  11196  xsubge0  12695  xmulgt0  12717  xmulge0  12718  xlemul1a  12722  sqlecan  13621  bernneq  13640  hashge1  13800  hashge2el2dif  13890  cnpart  14647  sqr0lem  14648  bitsfzo  15834  bitsmod  15835  bitsinv1lem  15840  pcge0  16253  prmreclem4  16310  prmreclem5  16311  isabvd  19659  abvtrivd  19679  isnzr2hash  20105  nmolb2d  23420  nmoi  23430  nmoleub  23433  nmo0  23437  ovolge0  24181  itg1ge0a  24411  fta1g  24867  plyrem  25000  taylfval  25053  abelthlem2  25126  sinq12ge0  25200  relogrn  25252  logneg  25278  cxpge0  25373  amgmlem  25674  bposlem5  25971  lgsdir2lem2  26009  2lgsoddprmlem3  26097  rpvmasumlem  26170  eupth2lem3lem3  28114  eupth2lemb  28121  blocnilem  28686  pjssge0ii  29564  unierri  29986  xlt2addrd  30605  locfinref  31312  esumcst  31550  ballotlem5  31985  poimirlem23  35360  poimirlem25  35362  poimirlem26  35363  poimirlem27  35364  poimirlem28  35365  itgaddnclem2  35396  pell14qrgt0  40173  monotoddzzfi  40256  rmxypos  40261  rmygeid  40278  stoweidlem18  43026  stoweidlem55  43063  wallispi2lem1  43079  fourierdlem62  43176  fourierdlem103  43217  fourierdlem104  43218  fourierswlem  43238  pgrpgt2nabl  45135  pw2m1lepw2m1  45294  amgmwlem  45721