Theorem eqbrtrdi 5141

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

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  eqbrtrrdi  5142  domunsn  9068  mapdom1  9083  mapdom2  9089  pm54.43  9930  infmap2  10146  inar1  10704  gruina  10747  nn0ledivnn  13042  xltnegi  13152  leexp1a  14116  discr  14181  facwordi  14230  faclbnd3  14233  hashgt12el  14363  hashle2pr  14418  cnpart  15182  geomulcvg  15818  dvds1  16265  ramz2  16971  ramz  16972  gex1  19505  sylow2a  19533  en1top  22904  en2top  22905  hmph0  23715  ptcmplem2  23973  dscmet  24493  dscopn  24494  xrge0tsms2  24757  htpycc  24912  pcohtpylem  24952  pcopt  24955  pcopt2  24956  pcoass  24957  pcorevlem  24959  vitalilem5  25546  dvef  25917  dveq0  25938  dv11cn  25939  deg1lt0  26029  ply1rem  26104  fta1g  26108  plyremlem  26245  aalioulem3  26275  pige3ALT  26462  relogrn  26503  logneg  26530  cxpaddlelem  26694  mule1  27091  ppiub  27148  dchrabs2  27206  bposlem1  27228  zabsle1  27240  lgseisen  27323  lgsquadlem2  27325  rpvmasumlem  27431  qabvle  27569  ostth3  27582  precsexlem9  28157  nnsrecgt0d  28283  0reno  28401  colinearalg  28890  eengstr  28960  clwwlknon1le1  30080  eucrct2eupth  30224  nmosetn0  30744  nmoo0  30770  siii  30832  bcsiALT  31158  branmfn  32084  fzo0opth  32778  drngidlhash  33398  m1pmeq  33545  cos9thpiminplylem1  33765  esumrnmpt2  34051  ballotlemrc  34515  pthhashvtx  35108  subfacval3  35169  sconnpi1  35219  fz0n  35711  poimirlem31  37638  itg2addnclem  37658  ftc1anc  37688  safesnsupfidom1o  43399  radcnvrat  44296  infxr  45356  stoweidlem18  46009  stoweidlem55  46046  fourierdlem62  46159  fourierswlem  46221  exple2lt6  48345  fvconstdomi  48873  f1omoALT  48876  indthincALT  49445