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  19497  sylow2a  19525  en1top  22847  en2top  22848  hmph0  23658  ptcmplem2  23916  dscmet  24436  dscopn  24437  xrge0tsms2  24700  htpycc  24855  pcohtpylem  24895  pcopt  24898  pcopt2  24899  pcoass  24900  pcorevlem  24902  vitalilem5  25489  dvef  25860  dveq0  25881  dv11cn  25882  deg1lt0  25972  ply1rem  26047  fta1g  26051  plyremlem  26188  aalioulem3  26218  pige3ALT  26405  relogrn  26446  logneg  26473  cxpaddlelem  26637  mule1  27034  ppiub  27091  dchrabs2  27149  bposlem1  27171  zabsle1  27183  lgseisen  27266  lgsquadlem2  27268  rpvmasumlem  27374  qabvle  27512  ostth3  27525  precsexlem9  28093  nnsrecgt0d  28219  0reno  28324  colinearalg  28813  eengstr  28883  clwwlknon1le1  30003  eucrct2eupth  30147  nmosetn0  30667  nmoo0  30693  siii  30755  bcsiALT  31081  branmfn  32007  fzo0opth  32701  drngidlhash  33378  m1pmeq  33525  cos9thpiminplylem1  33745  esumrnmpt2  34031  ballotlemrc  34495  pthhashvtx  35088  subfacval3  35149  sconnpi1  35199  fz0n  35691  poimirlem31  37618  itg2addnclem  37638  ftc1anc  37668  safesnsupfidom1o  43379  radcnvrat  44276  infxr  45336  stoweidlem18  45989  stoweidlem55  46026  fourierdlem62  46139  fourierswlem  46201  exple2lt6  48325  fvconstdomi  48853  f1omoALT  48856  indthincALT  49425