Theorem eqbrtrrid 5145

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 2763	. 2 ⊢ 𝐶 = 𝐶
4	1, 2, 3	3brtr3g 5142	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  enpr1g  9086  undom  9120  fidomdm  9359  resfifsupp  9424  prdom2  10122  infdju1  10305  infdif  10323  cfslb2n  10383  fin56  10508  dmct  10639  dmctOLD  10640  gchxpidm  10791  rankcf  10899  r1tskina  10904  tskuni  10905  ltsonq  11091  addgt0  11840  addgegt0  11841  addgtge0  11842  addge0  11843  expge1  14280  fsumrlim  16019  isumsup  16057  climcndslem1  16059  fprodge1  16203  3dvds  16542  bitsinv1lem  16652  phicl2  16986  frgpnabllem1  20129  lt6abl  20151  pgpfaclem2  20340  unitmulcl  20652  xrsdsreclblem  21761  znidomb  21911  lindfres  22173  gsumply1eq  22671  abrexct  23817  2ndcdisj2  23820  hmphindis  24160  tsms0  24505  tgptsmscls  24513  metustexhalf  24919  xrhmeo  25311  pcoass  25389  ovoliunlem1  25867  ismbl2  25892  voliunlem2  25916  ioombl1lem4  25926  itg2ge0  26100  itg2addlem  26123  itgge0  26175  dvfsumrlimge0  26394  abelthlem1  26804  abelthlem2  26805  pilem2  26825  cos0pilt1  26906  rplogcl  26978  logge0  26979  argimgt0  26986  logdivlti  26994  logf1o2  27024  dvlog2lem  27026  ang180lem3  27185  atanlogaddlem  27287  atanlogsublem  27289  atantan  27297  atans2  27305  cxploglim2  27352  emcllem6  27374  emcllem7  27375  lgamgulmlem2  27403  ftalem1  27446  ftalem2  27447  ppinncl  27547  chtrpcl  27548  vmalelog  27578  chtub  27585  logfacubnd  27594  logfacbnd3  27596  logfacrlim  27597  logexprlim  27598  mersenne  27600  perfectlem2  27603  bpos1lem  27655  bposlem1  27657  bposlem2  27658  bposlem3  27659  bposlem4  27660  bposlem5  27661  bposlem6  27662  lgseisen  27752  lgsquadlem1  27753  chebbnd1lem1  27842  chebbnd1lem3  27844  rpvmasumlem  27860  dchrvmasumlem2  27871  dchrvmasumlema  27873  dchrvmasumiflem1  27874  dchrisum0flblem2  27882  dchrisum0fno1  27884  dchrisum0re  27886  dirith2  27901  logdivsum  27906  mulog2sumlem1  27907  mulog2sumlem2  27908  log2sumbnd  27917  chpdifbndlem1  27926  chpdifbndlem2  27927  logdivbnd  27929  selberg3lem1  27930  pntpbnd1a  27958  pntpbnd2  27960  pntibndlem3  27965  pntlemn  27973  pntlemj  27976  pntlemk  27979  pnt  27987  fltoprmlem2  28040  addsgt0d  28446  ltmulnegs1d  28608  absmuls  28676  abssge0  28677  leabss  28680  nnsge1  28775  bdayfinbndlem1  28899  tgldimor  29011  axlowdim  29585  minvecolem4  31528  abrexctf  33396  nndiffz1  33464  wrdt2ind  33602  xrge0addgt0  33667  elrgspnlem2  33893  ply1coedeg  34217  drngdimgt0  34354  extdgfialglem2  34429  cos9thpiminplylem1  34518  esumcvg2  34823  inelcarsg  35047  carsgclctunlem2  35055  signsply0  35284  signsvtn  35317  erdsze2lem2  36170  lcmineqlem23  43360  lcmineqlem  43361  aks4d1p1p6  43382  aks4d1p1  43385  aks5lem2  43496  pellqrex  44146  reglogltb  44158  reglogleb  44159  rmspecnonsq  44174  rmspecpos  44183  areaquad  44473  hashnzfz2  45560  binomcxplemdvbinom  45592  binomcxplemnotnn0  45595  fmul01  46859  climconstmpt  46935  stoweidlem26  47303  stoweidlem44  47321  stoweidlem45  47322  wallispilem3  47344  wallispi  47347  stirlinglem11  47361  dirkertrigeqlem1  47375  dirkertrigeqlem3  47377  fourierdlem80  47463  fourierdlem102  47485  fourierdlem107  47490  fourierdlem114  47497  etransclem46  47557  fmtnoge3  48882  fmtno4prmfac  48924  perfectALTVlem2  49087  gboge9  49129  mogoldbb  49150  tgoldbach  49182  gpg3kgrtriexlem3  49450  gpg3kgrtriexlem6  49453  nnolog2flm1  50027