Theorem eqbrtrdi 5150

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

Syntax hints:   → wi 4   = wceq 1570   class class class wbr 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is referenced by:  eqbrtrrdi  5151  domunsn  9111  mapdom1  9126  mapdom2  9132  pm54.43  9983  infmap2  10196  inar1  10755  gruina  10798  nn0ledivnn  13126  xltnegi  13237  leexp1a  14207  discr  14272  facwordi  14321  faclbnd3  14324  hashgt12el  14455  hashle2pr  14510  cnpart  15287  geomulcvg  15926  dvds1  16372  ramz2  17079  ramz  17080  gex1  19656  sylow2a  19684  en1top  23141  en2top  23142  hmph0  23952  ptcmplem2  24210  dscmet  24729  dscopn  24730  xrge0tsms2  24993  htpycc  25139  pcohtpylem  25178  pcopt  25181  pcopt2  25182  pcoass  25183  pcorevlem  25185  vitalilem5  25771  dvef  26139  dveq0  26159  dv11cn  26160  deg1lt0  26248  ply1rem  26323  fta1g  26327  plyremlem  26465  aalioulem3  26497  pige3ALT  26685  relogrn  26726  logneg  26753  cxpaddlelem  26916  mule1  27312  ppiub  27368  dchrabs2  27426  bposlem1  27448  zabsle1  27460  lgseisen  27543  lgsquadlem2  27545  rpvmasumlem  27651  qabvle  27789  ostth3  27802  precsexlem9  28408  nnsrecgt0d  28544  colinearalg  29260  eengstr  29330  clwwlknon1le1  30452  eucrct2eupth  30596  nmosetn0  31117  nmoo0  31143  siii  31205  bcsiALT  31531  branmfn  32457  fzo0opth  33148  drngidlhash  33741  fldlring  33789  m1pmeq  33875  cos9thpiminplylem1  34172  esumrnmpt2  34458  ballotlemrc  34921  pthhashvtx  35620  subfacval3  35681  sconnpi1  35731  fz0n  36223  poimirlem31  38302  itg2addnclem  38322  ftc1anc  38352  safesnsupfidom1o  44143  radcnvrat  45024  infxr  46082  stoweidlem18  46732  stoweidlem55  46769  fourierdlem62  46882  fourierswlem  46944  chnsubseqwl  47595  exple2lt6  49144  fvconstdomi  49670  f1omoALT  49673  indthincALT  50241