Theorem breqtrrid 5123

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  r1sdom  9698  alephordilem1  9995  mulge0  11668  xsubge0  13213  xmulgt0  13235  xmulge0  13236  xlemul1a  13240  sqlecan  14171  bernneq  14191  hashge1  14351  hashge2el2dif  14442  cnpart  15202  sqrt0  15203  bitsfzo  16404  bitsmod  16405  bitsinv1lem  16410  pcge0  16833  prmreclem4  16890  prmreclem5  16891  isnzr2hash  20496  isabvd  20789  abvtrivd  20809  nmolb2d  24683  nmoi  24693  nmoleub  24696  nmo0  24700  ovolge0  25448  itg1ge0a  25678  fta1g  26135  plyrem  26271  taylfval  26324  abelthlem2  26397  sinq12ge0  26472  relogrn  26525  logneg  26552  cxpge0  26647  amgmlem  26953  bposlem5  27251  lgsdir2lem2  27289  2lgsoddprmlem3  27377  rpvmasumlem  27450  mulsge0d  28138  expsgt0  28429  eupth2lem3lem3  30300  eupth2lemb  30307  blocnilem  30875  pjssge0ii  31753  unierri  32175  xlt2addrd  32832  2sqr3minply  33924  locfinref  33985  esumcst  34207  ballotlem5  34644  poimirlem23  37964  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  itgaddnclem2  38000  sn-recgt0d  42922  pell14qrgt0  43287  monotoddzzfi  43370  rmxypos  43375  rmygeid  43392  stoweidlem18  46446  stoweidlem55  46483  wallispi2lem1  46499  fourierdlem62  46596  fourierdlem103  46637  fourierdlem104  46638  fourierswlem  46658  2ltceilhalf  47780  ceilhalfnn  47788  pgrpgt2nabl  48842  pw2m1lepw2m1  48996  amgmwlem  50277