Theorem breqtrrid 5147

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  r1sdom  9759  alephordilem1  10079  mulge0  11759  xsubge0  13315  xmulgt0  13337  xmulge0  13338  xlemul1a  13342  sqlecan  14275  bernneq  14295  hashge1  14455  hashge2el2dif  14547  cnpart  15329  sqrt0  15330  bitsfzo  16529  bitsmod  16530  bitsinv1lem  16535  pcge0  16958  prmreclem4  17015  prmreclem5  17016  isnzr2hash  20681  isabvd  20979  abvtrivd  20999  nmolb2d  24945  nmoi  24955  nmoleub  24958  nmo0  24962  ovolge0  25710  itg1ge0a  25940  fta1g  26397  plyrem  26536  taylfval  26592  abelthlem2  26665  sinq12ge0  26743  relogrn  26796  logneg  26823  cxpge0  26918  amgmlem  27224  bposlem5  27522  lgsdir2lem2  27560  2lgsoddprmlem3  27648  rpvmasumlem  27721  mulsge0d  28409  expsgt0  28700  eupth2lem3lem3  30696  eupth2lemb  30703  blocnilem  31271  pjssge0ii  32149  unierri  32571  xlt2addrd  33217  2sqr3minply  34277  locfinref  34338  esumcst  34560  ballotlem5  34998  poimirlem23  38379  poimirlem25  38381  poimirlem26  38382  poimirlem27  38383  poimirlem28  38384  itgaddnclem2  38415  sn-recgt0d  43352  pell14qrgt0  43687  monotoddzzfi  43770  rmxypos  43775  rmygeid  43792  stoweidlem18  46833  stoweidlem55  46870  wallispi2lem1  46886  fourierdlem62  46983  fourierdlem103  47024  fourierdlem104  47025  fourierswlem  47045  2ltceilhalf  48207  ceilhalfnn  48215  pgrpgt2nabl  49283  pw2m1lepw2m1  49437  amgmwlem  50807