Theorem breqtrrid 5068

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

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

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 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  r1sdom  9187  alephordilem1  9484  mulge0  11147  xsubge0  12642  xmulgt0  12664  xmulge0  12665  xlemul1a  12669  sqlecan  13567  bernneq  13586  hashge1  13746  hashge2el2dif  13834  cnpart  14591  sqr0lem  14592  bitsfzo  15774  bitsmod  15775  bitsinv1lem  15780  pcge0  16188  prmreclem4  16245  prmreclem5  16246  isabvd  19584  abvtrivd  19604  isnzr2hash  20030  nmolb2d  23324  nmoi  23334  nmoleub  23337  nmo0  23341  ovolge0  24085  itg1ge0a  24315  fta1g  24768  plyrem  24901  taylfval  24954  abelthlem2  25027  sinq12ge0  25101  relogrn  25153  logneg  25179  cxpge0  25274  amgmlem  25575  bposlem5  25872  lgsdir2lem2  25910  2lgsoddprmlem3  25998  rpvmasumlem  26071  eupth2lem3lem3  28015  eupth2lemb  28022  blocnilem  28587  pjssge0ii  29465  unierri  29887  xlt2addrd  30508  locfinref  31194  esumcst  31432  ballotlem5  31867  poimirlem23  35080  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  itgaddnclem2  35116  pell14qrgt0  39800  monotoddzzfi  39883  rmxypos  39888  rmygeid  39905  stoweidlem18  42660  stoweidlem55  42697  wallispi2lem1  42713  fourierdlem62  42810  fourierdlem103  42851  fourierdlem104  42852  fourierswlem  42872  pgrpgt2nabl  44768  pw2m1lepw2m1  44929  amgmwlem  45330