Theorem eqbrtrrid 5140

Description: A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)

Hypotheses

Ref	Expression
eqbrtrrid.1	⊢ 𝐵 = 𝐴
eqbrtrrid.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
eqbrtrrid	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrrid

Step	Hyp	Ref	Expression
1		eqbrtrrid.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrrid.1	. 2 ⊢ 𝐵 = 𝐴
3		eqid 2760	. 2 ⊢ 𝐶 = 𝐶
4	1, 2, 3	3brtr3g 5137	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  enpr1g  9050  undom  9084  fidomdm  9323  resfifsupp  9389  prdom2  10085  infdju1  10268  infdif  10286  cfslb2n  10346  fin56  10471  dmct  10602  dmctOLD  10603  gchxpidm  10754  rankcf  10862  r1tskina  10867  tskuni  10868  ltsonq  11054  addgt0  11802  addgegt0  11803  addgtge0  11804  addge0  11805  expge1  14242  fsumrlim  15978  isumsup  16016  climcndslem1  16018  fprodge1  16162  3dvds  16501  bitsinv1lem  16611  phicl2  16945  frgpnabllem1  20087  lt6abl  20109  pgpfaclem2  20298  unitmulcl  20610  xrsdsreclblem  21719  znidomb  21867  lindfres  22129  gsumply1eq  22627  abrexct  23773  2ndcdisj2  23776  hmphindis  24116  tsms0  24461  tgptsmscls  24469  metustexhalf  24875  xrhmeo  25267  pcoass  25345  ovoliunlem1  25823  ismbl2  25848  voliunlem2  25872  ioombl1lem4  25882  itg2ge0  26056  itg2addlem  26079  itgge0  26131  dvfsumrlimge0  26350  abelthlem1  26758  abelthlem2  26759  pilem2  26779  cos0pilt1  26860  rplogcl  26932  logge0  26933  argimgt0  26940  logdivlti  26948  logf1o2  26978  dvlog2lem  26980  ang180lem3  27139  atanlogaddlem  27241  atanlogsublem  27243  atantan  27251  atans2  27259  cxploglim2  27306  emcllem6  27328  emcllem7  27329  lgamgulmlem2  27357  ftalem1  27400  ftalem2  27401  ppinncl  27501  chtrpcl  27502  vmalelog  27532  chtub  27539  logfacubnd  27548  logfacbnd3  27550  logfacrlim  27551  logexprlim  27552  mersenne  27554  perfectlem2  27557  bpos1lem  27609  bposlem1  27611  bposlem2  27612  bposlem3  27613  bposlem4  27614  bposlem5  27615  bposlem6  27616  lgseisen  27706  lgsquadlem1  27707  chebbnd1lem1  27796  chebbnd1lem3  27798  rpvmasumlem  27814  dchrvmasumlem2  27825  dchrvmasumlema  27827  dchrvmasumiflem1  27828  dchrisum0flblem2  27836  dchrisum0fno1  27838  dchrisum0re  27840  dirith2  27855  logdivsum  27860  mulog2sumlem1  27861  mulog2sumlem2  27862  log2sumbnd  27871  chpdifbndlem1  27880  chpdifbndlem2  27881  logdivbnd  27883  selberg3lem1  27884  pntpbnd1a  27912  pntpbnd2  27914  pntibndlem3  27919  pntlemn  27927  pntlemj  27930  pntlemk  27933  pnt  27941  flt4lem7  27989  fltoprmlem2  27994  addsgt0d  28400  ltmulnegs1d  28562  absmuls  28630  abssge0  28631  leabss  28634  nnsge1  28729  bdayfinbndlem1  28853  tgldimor  28965  axlowdim  29539  minvecolem4  31482  abrexctf  33351  nndiffz1  33420  wrdt2ind  33558  xrge0addgt0  33620  elrgspnlem2  33846  ply1coedeg  34163  drngdimgt0  34292  extdgfialglem2  34367  cos9thpiminplylem1  34456  esumcvg2  34761  inelcarsg  34985  carsgclctunlem2  34993  signsply0  35222  signsvtn  35255  erdsze2lem2  36011  lcmineqlem23  43144  lcmineqlem  43145  aks4d1p1p6  43166  aks4d1p1  43169  aks5lem2  43280  pellqrex  43928  reglogltb  43940  reglogleb  43941  rmspecnonsq  43956  rmspecpos  43965  areaquad  44260  hashnzfz2  45347  binomcxplemdvbinom  45379  binomcxplemnotnn0  45382  fmul01  46634  climconstmpt  46710  stoweidlem26  47078  stoweidlem44  47096  stoweidlem45  47097  wallispilem3  47119  wallispi  47122  stirlinglem11  47136  dirkertrigeqlem1  47150  dirkertrigeqlem3  47152  fourierdlem80  47238  fourierdlem102  47260  fourierdlem107  47265  fourierdlem114  47272  etransclem46  47332  fmtnoge3  48657  fmtno4prmfac  48699  perfectALTVlem2  48862  gboge9  48904  mogoldbb  48925  tgoldbach  48957  gpg3kgrtriexlem3  49225  gpg3kgrtriexlem6  49228  nnolog2flm1  49744