Theorem breqtrrid 5204

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  r1sdom  9843  alephordilem1  10142  mulge0  11808  xsubge0  13323  xmulgt0  13345  xmulge0  13346  xlemul1a  13350  sqlecan  14258  bernneq  14278  hashge1  14438  hashge2el2dif  14529  cnpart  15289  sqrt0  15290  bitsfzo  16481  bitsmod  16482  bitsinv1lem  16487  pcge0  16909  prmreclem4  16966  prmreclem5  16967  isnzr2hash  20545  isabvd  20835  abvtrivd  20855  nmolb2d  24760  nmoi  24770  nmoleub  24773  nmo0  24777  ovolge0  25535  itg1ge0a  25766  fta1g  26229  plyrem  26365  taylfval  26418  abelthlem2  26494  sinq12ge0  26568  relogrn  26621  logneg  26648  cxpge0  26743  amgmlem  27051  bposlem5  27350  lgsdir2lem2  27388  2lgsoddprmlem3  27476  rpvmasumlem  27549  mulsge0d  28190  expsgt0  28433  eupth2lem3lem3  30262  eupth2lemb  30269  blocnilem  30836  pjssge0ii  31714  unierri  32136  xlt2addrd  32765  2sqr3minply  33738  locfinref  33787  esumcst  34027  ballotlem5  34464  poimirlem23  37603  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  itgaddnclem2  37639  pell14qrgt0  42815  monotoddzzfi  42899  rmxypos  42904  rmygeid  42921  stoweidlem18  45939  stoweidlem55  45976  wallispi2lem1  45992  fourierdlem62  46089  fourierdlem103  46130  fourierdlem104  46131  fourierswlem  46151  pgrpgt2nabl  48091  pw2m1lepw2m1  48249  amgmwlem  48896