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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109

This theorem is used by:  eqbrtrrdi  5151  domunsn  9184  mapdom1  9199  mapdom2  9205  pm54.43  10121  infmap2  10334  inar1  10899  gruina  10942  nn0ledivnn  13275  xltnegi  13386  leexp1a  14358  discr  14425  facwordi  14474  faclbnd3  14477  hashgt12el  14608  hashle2pr  14663  cnpart  15450  geomulcvg  16089  dvds1  16533  ramz2  17246  ramz  17247  gex1  19856  sylow2a  19884  en1top  23357  en2top  23358  hmph0  24169  ptcmplem2  24427  dscmet  24946  dscopn  24947  xrge0tsms2  25210  htpycc  25356  pcohtpylem  25395  pcopt  25398  pcopt2  25399  pcoass  25400  pcorevlem  25402  vitalilem5  25988  dvef  26355  dveq0  26375  dv11cn  26376  deg1lt0  26464  ply1rem  26539  fta1g  26543  plyremlem  26680  aalioulem3  26718  pige3ALT  26905  relogrn  26946  logneg  26973  cxpaddlelem  27136  mule1  27532  ppiub  27588  dchrabs2  27646  bposlem1  27668  zabsle1  27680  lgseisen  27763  lgsquadlem2  27765  rpvmasumlem  27871  qabvle  28009  ostth3  28022  precsexlem9  28658  nnsrecgt0d  28794  colinearalg  29545  eengstr  29615  pthhashvtx  30372  clwwlknon1le1  30749  eucrct2eupth  30903  nmosetn0  31424  nmoo0  31450  siii  31512  bcsiALT  31838  branmfn  32764  fzo0opth  33491  drngidlhash  34087  fldlring  34135  m1pmeq  34220  deg1le1  34238  rngunsnply1chr2lem3  34252  cos9thpiminplylem1  34525  esumrnmpt2  34811  ballotlemrc  35274  subfacval3  36162  sconnpi1  36212  fz0n  36711  poimirlem31  38837  itg2addnclem  38857  ftc1anc  38887  safesnsupfidom1o  44679  radcnvrat  45559  infxr  46651  stoweidlem18  47301  stoweidlem55  47338  fourierdlem62  47451  fourierswlem  47513  chnsubseqwl  48162  exple2lt6  49807  fvconstdomi  50337  f1omoALT  50340  indthincALT  50929