Theorem breqtrrid 5124

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 5123	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  r1sdom  9693  alephordilem1  9990  mulge0  11663  xsubge0  13208  xmulgt0  13230  xmulge0  13231  xlemul1a  13235  sqlecan  14166  bernneq  14186  hashge1  14346  hashge2el2dif  14437  cnpart  15197  sqrt0  15198  bitsfzo  16399  bitsmod  16400  bitsinv1lem  16405  pcge0  16828  prmreclem4  16885  prmreclem5  16886  isnzr2hash  20491  isabvd  20784  abvtrivd  20804  nmolb2d  24697  nmoi  24707  nmoleub  24710  nmo0  24714  ovolge0  25462  itg1ge0a  25692  fta1g  26149  plyrem  26286  taylfval  26339  abelthlem2  26414  sinq12ge0  26489  relogrn  26542  logneg  26569  cxpge0  26664  amgmlem  26971  bposlem5  27269  lgsdir2lem2  27307  2lgsoddprmlem3  27395  rpvmasumlem  27468  mulsge0d  28156  expsgt0  28447  eupth2lem3lem3  30319  eupth2lemb  30326  blocnilem  30894  pjssge0ii  31772  unierri  32194  xlt2addrd  32851  2sqr3minply  33944  locfinref  34005  esumcst  34227  ballotlem5  34664  poimirlem23  37984  poimirlem25  37986  poimirlem26  37987  poimirlem27  37988  poimirlem28  37989  itgaddnclem2  38020  sn-recgt0d  42942  pell14qrgt0  43311  monotoddzzfi  43394  rmxypos  43399  rmygeid  43416  stoweidlem18  46470  stoweidlem55  46507  wallispi2lem1  46523  fourierdlem62  46620  fourierdlem103  46661  fourierdlem104  46662  fourierswlem  46682  2ltceilhalf  47798  ceilhalfnn  47806  pgrpgt2nabl  48860  pw2m1lepw2m1  49014  amgmwlem  50295