Theorem eqbrtrrid 5152

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

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

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115

This theorem is used by:  enpr1g  9029  undom  9063  fidomdm  9301  resfifsupp  9367  prdom2  10009  infdju1  10192  infdif  10210  cfslb2n  10270  fin56  10395  dmct  10526  gchxpidm  10672  rankcf  10780  r1tskina  10785  tskuni  10786  ltsonq  10972  addgt0  11718  addgegt0  11719  addgtge0  11720  addge0  11721  expge1  14155  fsumrlim  15889  isumsup  15927  climcndslem1  15929  fprodge1  16075  3dvds  16414  bitsinv1lem  16524  phicl2  16852  frgpnabllem1  19974  lt6abl  19996  pgpfaclem2  20185  unitmulcl  20495  xrsdsreclblem  21600  znidomb  21748  lindfres  22010  gsumply1eq  22506  2ndcdisj2  23651  hmphindis  23991  tsms0  24336  tgptsmscls  24344  metustexhalf  24750  xrhmeo  25142  pcoass  25220  ovoliunlem1  25698  ismbl2  25723  voliunlem2  25747  ioombl1lem4  25757  itg2ge0  25931  itg2addlem  25954  itgge0  26007  dvfsumrlimge0  26226  abelthlem1  26631  abelthlem2  26632  pilem2  26652  cos0pilt1  26734  rplogcl  26806  logge0  26807  argimgt0  26814  logdivlti  26822  logf1o2  26852  dvlog2lem  26854  ang180lem3  27013  atanlogaddlem  27115  atanlogsublem  27117  atantan  27125  atans2  27133  cxploglim2  27180  emcllem6  27202  emcllem7  27203  lgamgulmlem2  27231  ftalem1  27274  ftalem2  27275  ppinncl  27375  chtrpcl  27376  vmalelog  27406  chtub  27413  logfacubnd  27422  logfacbnd3  27424  logfacrlim  27425  logexprlim  27426  mersenne  27428  perfectlem2  27431  bpos1lem  27483  bposlem1  27485  bposlem2  27486  bposlem3  27487  bposlem4  27488  bposlem5  27489  bposlem6  27490  lgseisen  27580  lgsquadlem1  27581  chebbnd1lem1  27670  chebbnd1lem3  27672  rpvmasumlem  27688  dchrvmasumlem2  27699  dchrvmasumlema  27701  dchrvmasumiflem1  27702  dchrisum0flblem2  27710  dchrisum0fno1  27712  dchrisum0re  27714  dirith2  27729  logdivsum  27734  mulog2sumlem1  27735  mulog2sumlem2  27736  log2sumbnd  27745  chpdifbndlem1  27754  chpdifbndlem2  27755  logdivbnd  27757  selberg3lem1  27758  pntpbnd1a  27786  pntpbnd2  27788  pntibndlem3  27793  pntlemn  27801  pntlemj  27804  pntlemk  27807  pnt  27815  addsgt0d  28244  ltmulnegs1d  28406  absmuls  28474  abssge0  28475  leabss  28478  nnsge1  28573  bdayfinbndlem1  28697  tgldimor  28808  axlowdim  29348  minvecolem4  31269  abrexct  33097  abrexctf  33099  nndiffz1  33168  wrdt2ind  33306  xrge0addgt0  33368  elrgspnlem2  33594  ply1coedeg  33910  drngdimgt0  34039  extdgfialglem2  34114  cos9thpiminplylem1  34203  esumcvg2  34508  inelcarsg  34733  carsgclctunlem2  34741  signsply0  34970  signsvtn  35003  erdsze2lem2  35717  lcmineqlem23  42859  lcmineqlem  42860  aks4d1p1p6  42881  aks4d1p1  42884  aks5lem2  42995  flt4lem7  43432  pellqrex  43647  reglogltb  43659  reglogleb  43660  rmspecnonsq  43675  rmspecpos  43684  areaquad  43984  hashnzfz2  45072  binomcxplemdvbinom  45104  binomcxplemnotnn0  45107  fmul01  46337  climconstmpt  46413  stoweidlem26  46781  stoweidlem44  46799  stoweidlem45  46800  wallispilem3  46822  wallispi  46825  stirlinglem11  46839  dirkertrigeqlem1  46853  dirkertrigeqlem3  46855  fourierdlem80  46941  fourierdlem102  46963  fourierdlem107  46968  fourierdlem114  46975  etransclem46  47035  fmtnoge3  48323  fmtno4prmfac  48365  perfectALTVlem2  48528  gboge9  48570  mogoldbb  48591  tgoldbach  48623  gpg3kgrtriexlem3  48891  gpg3kgrtriexlem6  48894  nnolog2flm1  49411