Theorem eqbrtrdi 5109

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  eqbrtrrdi  5110  domunsn  8863  mapdom1  8878  mapdom2  8884  pm54.43  9690  infmap2  9905  inar1  10462  gruina  10505  nn0ledivnn  12772  xltnegi  12879  leexp1a  13821  discr  13883  facwordi  13931  faclbnd3  13934  hashgt12el  14065  hashle2pr  14119  cnpart  14879  geomulcvg  15516  dvds1  15956  ramz2  16653  ramz  16654  gex1  19111  sylow2a  19139  en1top  22042  en2top  22043  hmph0  22854  ptcmplem2  23112  dscmet  23634  dscopn  23635  xrge0tsms2  23904  htpycc  24049  pcohtpylem  24088  pcopt  24091  pcopt2  24092  pcoass  24093  pcorevlem  24095  vitalilem5  24681  dvef  25049  dveq0  25069  dv11cn  25070  deg1lt0  25161  ply1rem  25233  fta1g  25237  plyremlem  25369  aalioulem3  25399  pige3ALT  25581  relogrn  25622  logneg  25648  cxpaddlelem  25809  mule1  26202  ppiub  26257  dchrabs2  26315  bposlem1  26337  zabsle1  26349  lgseisen  26432  lgsquadlem2  26434  rpvmasumlem  26540  qabvle  26678  ostth3  26691  colinearalg  27181  eengstr  27251  clwwlknon1le1  28366  eucrct2eupth  28510  nmosetn0  29028  nmoo0  29054  siii  29116  bcsiALT  29442  branmfn  30368  esumrnmpt2  31936  ballotlemrc  32397  pthhashvtx  32989  subfacval3  33051  sconnpi1  33101  fz0n  33602  poimirlem31  35735  itg2addnclem  35755  ftc1anc  35785  radcnvrat  41821  infxr  42796  stoweidlem18  43449  stoweidlem55  43486  fourierdlem62  43599  fourierswlem  43661  exple2lt6  45588  fvconstdomi  46075  f1omoALT  46077  indthincALT  46222