Theorem breqtrrid 5186

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149

This theorem is referenced by:  r1sdom  9812  alephordilem1  10111  mulge0  11779  xsubge0  13300  xmulgt0  13322  xmulge0  13323  xlemul1a  13327  sqlecan  14245  bernneq  14265  hashge1  14425  hashge2el2dif  14516  cnpart  15276  sqrt0  15277  bitsfzo  16469  bitsmod  16470  bitsinv1lem  16475  pcge0  16896  prmreclem4  16953  prmreclem5  16954  isnzr2hash  20536  isabvd  20830  abvtrivd  20850  nmolb2d  24755  nmoi  24765  nmoleub  24768  nmo0  24772  ovolge0  25530  itg1ge0a  25761  fta1g  26224  plyrem  26362  taylfval  26415  abelthlem2  26491  sinq12ge0  26565  relogrn  26618  logneg  26645  cxpge0  26740  amgmlem  27048  bposlem5  27347  lgsdir2lem2  27385  2lgsoddprmlem3  27473  rpvmasumlem  27546  mulsge0d  28187  expsgt0  28430  eupth2lem3lem3  30259  eupth2lemb  30266  blocnilem  30833  pjssge0ii  31711  unierri  32133  xlt2addrd  32769  2sqr3minply  33753  locfinref  33802  esumcst  34044  ballotlem5  34481  poimirlem23  37630  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  poimirlem28  37635  itgaddnclem2  37666  pell14qrgt0  42847  monotoddzzfi  42931  rmxypos  42936  rmygeid  42953  stoweidlem18  45974  stoweidlem55  46011  wallispi2lem1  46027  fourierdlem62  46124  fourierdlem103  46165  fourierdlem104  46166  fourierswlem  46186  2ltceilhalf  47950  pgrpgt2nabl  48211  pw2m1lepw2m1  48366  amgmwlem  49033