Theorem breqtrrid 5145

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  r1sdom  9727  alephordilem1  10026  mulge0  11696  xsubge0  13221  xmulgt0  13243  xmulge0  13244  xlemul1a  13248  sqlecan  14174  bernneq  14194  hashge1  14354  hashge2el2dif  14445  cnpart  15206  sqrt0  15207  bitsfzo  16405  bitsmod  16406  bitsinv1lem  16411  pcge0  16833  prmreclem4  16890  prmreclem5  16891  isnzr2hash  20428  isabvd  20721  abvtrivd  20741  nmolb2d  24606  nmoi  24616  nmoleub  24619  nmo0  24623  ovolge0  25382  itg1ge0a  25612  fta1g  26075  plyrem  26213  taylfval  26266  abelthlem2  26342  sinq12ge0  26417  relogrn  26470  logneg  26497  cxpge0  26592  amgmlem  26900  bposlem5  27199  lgsdir2lem2  27237  2lgsoddprmlem3  27325  rpvmasumlem  27398  mulsge0d  28049  expsgt0  28322  eupth2lem3lem3  30159  eupth2lemb  30166  blocnilem  30733  pjssge0ii  31611  unierri  32033  xlt2addrd  32682  2sqr3minply  33770  locfinref  33831  esumcst  34053  ballotlem5  34491  poimirlem23  37637  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  itgaddnclem2  37673  sn-recgt0d  42465  pell14qrgt0  42847  monotoddzzfi  42931  rmxypos  42936  rmygeid  42953  stoweidlem18  46016  stoweidlem55  46053  wallispi2lem1  46069  fourierdlem62  46166  fourierdlem103  46207  fourierdlem104  46208  fourierswlem  46228  2ltceilhalf  47326  ceilhalfnn  47334  pgrpgt2nabl  48351  pw2m1lepw2m1  48506  amgmwlem  49788