Theorem eqbrtrdi 5139

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

Syntax hints:   → wi 4   = wceq 1560   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  eqbrtrrdi  5140  domunsn  9099  mapdom1  9114  mapdom2  9120  pm54.43  9959  infmap2  10173  inar1  10733  gruina  10776  nn0ledivnn  13108  xltnegi  13219  leexp1a  14188  discr  14253  facwordi  14302  faclbnd3  14305  hashgt12el  14435  hashle2pr  14490  cnpart  15267  geomulcvg  15906  dvds1  16353  ramz2  17060  ramz  17061  gex1  19631  sylow2a  19659  en1top  23041  en2top  23042  hmph0  23852  ptcmplem2  24110  dscmet  24629  dscopn  24630  xrge0tsms2  24893  htpycc  25039  pcohtpylem  25078  pcopt  25081  pcopt2  25082  pcoass  25083  pcorevlem  25085  vitalilem5  25671  dvef  26039  dveq0  26059  dv11cn  26060  deg1lt0  26148  ply1rem  26223  fta1g  26227  plyremlem  26365  aalioulem3  26395  pige3ALT  26582  relogrn  26623  logneg  26650  cxpaddlelem  26813  mule1  27209  ppiub  27265  dchrabs2  27323  bposlem1  27345  zabsle1  27357  lgseisen  27440  lgsquadlem2  27442  rpvmasumlem  27548  qabvle  27686  ostth3  27699  precsexlem9  28305  nnsrecgt0d  28441  colinearalg  29108  eengstr  29178  clwwlknon1le1  30300  eucrct2eupth  30444  nmosetn0  30965  nmoo0  30991  siii  31053  bcsiALT  31379  branmfn  32305  fzo0opth  33002  drngidlhash  33617  fldlring  33692  m1pmeq  33778  cos9thpiminplylem1  34076  esumrnmpt2  34362  ballotlemrc  34825  pthhashvtx  35475  subfacval3  35536  sconnpi1  35586  fz0n  36078  poimirlem31  38147  itg2addnclem  38167  ftc1anc  38197  safesnsupfidom1o  43990  radcnvrat  44887  infxr  45939  stoweidlem18  46589  stoweidlem55  46626  fourierdlem62  46739  fourierswlem  46801  chnsubseqwl  47452  exple2lt6  48983  fvconstdomi  49510  f1omoALT  49513  indthincALT  50081