Theorem eqbrtrdi 5146

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  eqbrtrrdi  5147  domunsn  9091  mapdom1  9106  mapdom2  9112  pm54.43  9954  infmap2  10170  inar1  10728  gruina  10771  nn0ledivnn  13066  xltnegi  13176  leexp1a  14140  discr  14205  facwordi  14254  faclbnd3  14257  hashgt12el  14387  hashle2pr  14442  cnpart  15206  geomulcvg  15842  dvds1  16289  ramz2  16995  ramz  16996  gex1  19521  sylow2a  19549  en1top  22871  en2top  22872  hmph0  23682  ptcmplem2  23940  dscmet  24460  dscopn  24461  xrge0tsms2  24724  htpycc  24879  pcohtpylem  24919  pcopt  24922  pcopt2  24923  pcoass  24924  pcorevlem  24926  vitalilem5  25513  dvef  25884  dveq0  25905  dv11cn  25906  deg1lt0  25996  ply1rem  26071  fta1g  26075  plyremlem  26212  aalioulem3  26242  pige3ALT  26429  relogrn  26470  logneg  26497  cxpaddlelem  26661  mule1  27058  ppiub  27115  dchrabs2  27173  bposlem1  27195  zabsle1  27207  lgseisen  27290  lgsquadlem2  27292  rpvmasumlem  27398  qabvle  27536  ostth3  27549  precsexlem9  28117  nnsrecgt0d  28243  0reno  28348  colinearalg  28837  eengstr  28907  clwwlknon1le1  30030  eucrct2eupth  30174  nmosetn0  30694  nmoo0  30720  siii  30782  bcsiALT  31108  branmfn  32034  fzo0opth  32728  drngidlhash  33405  m1pmeq  33552  cos9thpiminplylem1  33772  esumrnmpt2  34058  ballotlemrc  34522  pthhashvtx  35115  subfacval3  35176  sconnpi1  35226  fz0n  35718  poimirlem31  37645  itg2addnclem  37665  ftc1anc  37695  safesnsupfidom1o  43406  radcnvrat  44303  infxr  45363  stoweidlem18  46016  stoweidlem55  46053  fourierdlem62  46166  fourierswlem  46228  exple2lt6  48352  fvconstdomi  48880  f1omoALT  48883  indthincALT  49452