Theorem eqbrtrdi 5144

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  eqbrtrrdi  5145  domunsn  9139  mapdom1  9154  mapdom2  9160  pm54.43  10075  infmap2  10288  inar1  10853  gruina  10896  nn0ledivnn  13228  xltnegi  13339  leexp1a  14311  discr  14377  facwordi  14426  faclbnd3  14429  hashgt12el  14560  hashle2pr  14615  cnpart  15400  geomulcvg  16038  dvds1  16482  ramz2  17195  ramz  17196  gex1  19798  sylow2a  19826  en1top  23295  en2top  23296  hmph0  24107  ptcmplem2  24365  dscmet  24884  dscopn  24885  xrge0tsms2  25148  htpycc  25294  pcohtpylem  25333  pcopt  25336  pcopt2  25337  pcoass  25338  pcorevlem  25340  vitalilem5  25926  dvef  26293  dveq0  26313  dv11cn  26314  deg1lt0  26402  ply1rem  26477  fta1g  26481  plyremlem  26618  aalioulem3  26654  pige3ALT  26841  relogrn  26882  logneg  26909  cxpaddlelem  27072  mule1  27468  ppiub  27524  dchrabs2  27582  bposlem1  27604  zabsle1  27616  lgseisen  27699  lgsquadlem2  27701  rpvmasumlem  27807  qabvle  27945  ostth3  27958  precsexlem9  28594  nnsrecgt0d  28730  colinearalg  29481  eengstr  29551  pthhashvtx  30308  clwwlknon1le1  30685  eucrct2eupth  30839  nmosetn0  31360  nmoo0  31386  siii  31448  bcsiALT  31774  branmfn  32700  fzo0opth  33388  drngidlhash  33976  fldlring  34024  m1pmeq  34110  cos9thpiminplylem1  34407  esumrnmpt2  34693  ballotlemrc  35156  subfacval3  35933  sconnpi1  35983  fz0n  36475  poimirlem31  38549  itg2addnclem  38569  ftc1anc  38599  safesnsupfidom1o  44402  radcnvrat  45283  infxr  46347  stoweidlem18  46997  stoweidlem55  47034  fourierdlem62  47147  fourierswlem  47209  chnsubseqwl  47858  exple2lt6  49445  fvconstdomi  49969  f1omoALT  49972  indthincALT  50540