Theorem eqbrtrdi 5182

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  eqbrtrrdi  5183  domunsn  9167  mapdom1  9182  mapdom2  9188  pm54.43  10041  infmap2  10257  inar1  10815  gruina  10858  nn0ledivnn  13148  xltnegi  13258  leexp1a  14215  discr  14279  facwordi  14328  faclbnd3  14331  hashgt12el  14461  hashle2pr  14516  cnpart  15279  geomulcvg  15912  dvds1  16356  ramz2  17062  ramz  17063  gex1  19609  sylow2a  19637  en1top  22991  en2top  22992  hmph0  23803  ptcmplem2  24061  dscmet  24585  dscopn  24586  xrge0tsms2  24857  htpycc  25012  pcohtpylem  25052  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  vitalilem5  25647  dvef  26018  dveq0  26039  dv11cn  26040  deg1lt0  26130  ply1rem  26205  fta1g  26209  plyremlem  26346  aalioulem3  26376  pige3ALT  26562  relogrn  26603  logneg  26630  cxpaddlelem  26794  mule1  27191  ppiub  27248  dchrabs2  27306  bposlem1  27328  zabsle1  27340  lgseisen  27423  lgsquadlem2  27425  rpvmasumlem  27531  qabvle  27669  ostth3  27682  precsexlem9  28239  nnsrecgt0d  28356  cutpw2  28417  pw2bday  28418  0reno  28429  colinearalg  28925  eengstr  28995  clwwlknon1le1  30120  eucrct2eupth  30264  nmosetn0  30784  nmoo0  30810  siii  30872  bcsiALT  31198  branmfn  32124  fzo0opth  32807  drngidlhash  33462  m1pmeq  33608  esumrnmpt2  34069  ballotlemrc  34533  pthhashvtx  35133  subfacval3  35194  sconnpi1  35244  fz0n  35731  poimirlem31  37658  itg2addnclem  37678  ftc1anc  37708  safesnsupfidom1o  43430  radcnvrat  44333  infxr  45378  stoweidlem18  46033  stoweidlem55  46070  fourierdlem62  46183  fourierswlem  46245  exple2lt6  48280  fvconstdomi  48791  f1omoALT  48793  indthincALT  49110