Theorem eqbrtrdi 5128

Description: A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)

Hypotheses

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

Assertion

Ref	Expression
eqbrtrdi	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrdi

Step	Hyp	Ref	Expression
1		eqbrtrdi.2	. 2 ⊢ 𝐵𝑅𝐶
2		eqbrtrdi.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 5099	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbiri 258	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  eqbrtrrdi  5129  domunsn  9040  mapdom1  9055  mapdom2  9061  pm54.43  9894  infmap2  10108  inar1  10666  gruina  10709  nn0ledivnn  13005  xltnegi  13115  leexp1a  14082  discr  14147  facwordi  14196  faclbnd3  14199  hashgt12el  14329  hashle2pr  14384  cnpart  15147  geomulcvg  15783  dvds1  16230  ramz2  16936  ramz  16937  gex1  19503  sylow2a  19531  en1top  22899  en2top  22900  hmph0  23710  ptcmplem2  23968  dscmet  24487  dscopn  24488  xrge0tsms2  24751  htpycc  24906  pcohtpylem  24946  pcopt  24949  pcopt2  24950  pcoass  24951  pcorevlem  24953  vitalilem5  25540  dvef  25911  dveq0  25932  dv11cn  25933  deg1lt0  26023  ply1rem  26098  fta1g  26102  plyremlem  26239  aalioulem3  26269  pige3ALT  26456  relogrn  26497  logneg  26524  cxpaddlelem  26688  mule1  27085  ppiub  27142  dchrabs2  27200  bposlem1  27222  zabsle1  27234  lgseisen  27317  lgsquadlem2  27319  rpvmasumlem  27425  qabvle  27563  ostth3  27576  precsexlem9  28153  nnsrecgt0d  28279  0reno  28399  colinearalg  28888  eengstr  28958  clwwlknon1le1  30081  eucrct2eupth  30225  nmosetn0  30745  nmoo0  30771  siii  30833  bcsiALT  31159  branmfn  32085  fzo0opth  32785  drngidlhash  33399  m1pmeq  33547  cos9thpiminplylem1  33795  esumrnmpt2  34081  ballotlemrc  34544  pthhashvtx  35172  subfacval3  35233  sconnpi1  35283  fz0n  35775  poimirlem31  37699  itg2addnclem  37719  ftc1anc  37749  safesnsupfidom1o  43458  radcnvrat  44355  infxr  45413  stoweidlem18  46064  stoweidlem55  46101  fourierdlem62  46214  fourierswlem  46276  exple2lt6  48403  fvconstdomi  48931  f1omoALT  48934  indthincALT  49503