Theorem breqtrrid 5138

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5100

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  r1sdom  9700  alephordilem1  9997  mulge0  11669  xsubge0  13190  xmulgt0  13212  xmulge0  13213  xlemul1a  13217  sqlecan  14146  bernneq  14166  hashge1  14326  hashge2el2dif  14417  cnpart  15177  sqrt0  15178  bitsfzo  16376  bitsmod  16377  bitsinv1lem  16382  pcge0  16804  prmreclem4  16861  prmreclem5  16862  isnzr2hash  20469  isabvd  20762  abvtrivd  20782  nmolb2d  24679  nmoi  24689  nmoleub  24692  nmo0  24696  ovolge0  25455  itg1ge0a  25685  fta1g  26148  plyrem  26286  taylfval  26339  abelthlem2  26415  sinq12ge0  26490  relogrn  26543  logneg  26570  cxpge0  26665  amgmlem  26973  bposlem5  27272  lgsdir2lem2  27310  2lgsoddprmlem3  27398  rpvmasumlem  27471  mulsge0d  28159  expsgt0  28450  eupth2lem3lem3  30323  eupth2lemb  30330  blocnilem  30898  pjssge0ii  31776  unierri  32198  xlt2addrd  32856  2sqr3minply  33964  locfinref  34025  esumcst  34247  ballotlem5  34684  poimirlem23  37923  poimirlem25  37925  poimirlem26  37926  poimirlem27  37927  poimirlem28  37928  itgaddnclem2  37959  sn-recgt0d  42876  pell14qrgt0  43245  monotoddzzfi  43328  rmxypos  43333  rmygeid  43350  stoweidlem18  46405  stoweidlem55  46442  wallispi2lem1  46458  fourierdlem62  46555  fourierdlem103  46596  fourierdlem104  46597  fourierswlem  46617  2ltceilhalf  47717  ceilhalfnn  47725  pgrpgt2nabl  48755  pw2m1lepw2m1  48909  amgmwlem  50190