Theorem breqtrrid 5140

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

Syntax hints:   → wi 4   = wceq 1562   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  r1sdom  9734  alephordilem1  10031  mulge0  11707  xsubge0  13266  xmulgt0  13288  xmulge0  13289  xlemul1a  13293  sqlecan  14224  bernneq  14244  hashge1  14404  hashge2el2dif  14495  cnpart  15269  sqrt0  15270  bitsfzo  16471  bitsmod  16472  bitsinv1lem  16477  pcge0  16900  prmreclem4  16957  prmreclem5  16958  isnzr2hash  20571  isabvd  20863  abvtrivd  20883  nmolb2d  24780  nmoi  24790  nmoleub  24793  nmo0  24797  ovolge0  25545  itg1ge0a  25775  fta1g  26232  plyrem  26371  taylfval  26424  abelthlem2  26497  sinq12ge0  26575  relogrn  26628  logneg  26655  cxpge0  26750  amgmlem  27056  bposlem5  27354  lgsdir2lem2  27392  2lgsoddprmlem3  27480  rpvmasumlem  27553  mulsge0d  28241  expsgt0  28532  eupth2lem3lem3  30434  eupth2lemb  30441  blocnilem  31009  pjssge0ii  31887  unierri  32309  xlt2addrd  32963  2sqr3minply  34079  locfinref  34140  esumcst  34362  ballotlem5  34799  poimirlem23  38147  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  poimirlem28  38152  itgaddnclem2  38183  sn-recgt0d  43104  pell14qrgt0  43441  monotoddzzfi  43524  rmxypos  43529  rmygeid  43546  stoweidlem18  46597  stoweidlem55  46634  wallispi2lem1  46650  fourierdlem62  46747  fourierdlem103  46788  fourierdlem104  46789  fourierswlem  46809  2ltceilhalf  47931  ceilhalfnn  47939  pgrpgt2nabl  48993  pw2m1lepw2m1  49147  amgmwlem  50428