Theorem eqbrtrdi 5149

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 5120	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbiri 258	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  eqbrtrrdi  5150  domunsn  9097  mapdom1  9112  mapdom2  9118  pm54.43  9961  infmap2  10177  inar1  10735  gruina  10778  nn0ledivnn  13073  xltnegi  13183  leexp1a  14147  discr  14212  facwordi  14261  faclbnd3  14264  hashgt12el  14394  hashle2pr  14449  cnpart  15213  geomulcvg  15849  dvds1  16296  ramz2  17002  ramz  17003  gex1  19528  sylow2a  19556  en1top  22878  en2top  22879  hmph0  23689  ptcmplem2  23947  dscmet  24467  dscopn  24468  xrge0tsms2  24731  htpycc  24886  pcohtpylem  24926  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  vitalilem5  25520  dvef  25891  dveq0  25912  dv11cn  25913  deg1lt0  26003  ply1rem  26078  fta1g  26082  plyremlem  26219  aalioulem3  26249  pige3ALT  26436  relogrn  26477  logneg  26504  cxpaddlelem  26668  mule1  27065  ppiub  27122  dchrabs2  27180  bposlem1  27202  zabsle1  27214  lgseisen  27297  lgsquadlem2  27299  rpvmasumlem  27405  qabvle  27543  ostth3  27556  precsexlem9  28124  nnsrecgt0d  28250  0reno  28355  colinearalg  28844  eengstr  28914  clwwlknon1le1  30037  eucrct2eupth  30181  nmosetn0  30701  nmoo0  30727  siii  30789  bcsiALT  31115  branmfn  32041  fzo0opth  32735  drngidlhash  33412  m1pmeq  33559  cos9thpiminplylem1  33779  esumrnmpt2  34065  ballotlemrc  34529  pthhashvtx  35122  subfacval3  35183  sconnpi1  35233  fz0n  35725  poimirlem31  37652  itg2addnclem  37672  ftc1anc  37702  safesnsupfidom1o  43413  radcnvrat  44310  infxr  45370  stoweidlem18  46023  stoweidlem55  46060  fourierdlem62  46173  fourierswlem  46235  exple2lt6  48356  fvconstdomi  48884  f1omoALT  48887  indthincALT  49456