Theorem syl6eqbr 5007

Description: A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)

Hypotheses

Ref	Expression
syl6eqbr.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6eqbr.2	⊢ 𝐵𝑅𝐶

Assertion

Ref	Expression
syl6eqbr	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem syl6eqbr

Step	Hyp	Ref	Expression
1		syl6eqbr.2	. 2 ⊢ 𝐵𝑅𝐶
2		syl6eqbr.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 4978	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbiri 259	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1525   class class class wbr 4968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-br 4969

This theorem is referenced by:  syl6eqbrr  5008  domunsn  8521  mapdom1  8536  mapdom2  8542  pm54.43  9282  infmap2  9493  inar1  10050  gruina  10093  nn0ledivnn  12356  xltnegi  12463  leexp1a  13393  discr  13455  facwordi  13503  faclbnd3  13506  hashgt12el  13635  hashle2pr  13685  cnpart  14437  geomulcvg  15069  dvds1  15506  ramz2  16193  ramz  16194  gex1  18450  sylow2a  18478  en1top  21280  en2top  21281  hmph0  22091  ptcmplem2  22349  dscmet  22869  dscopn  22870  xrge0tsms2  23130  htpycc  23271  pcohtpylem  23310  pcopt  23313  pcopt2  23314  pcoass  23315  pcorevlem  23317  vitalilem5  23900  dvef  24264  dveq0  24284  dv11cn  24285  deg1lt0  24372  ply1rem  24444  fta1g  24448  plyremlem  24580  aalioulem3  24610  pige3ALT  24792  relogrn  24830  logneg  24856  cxpaddlelem  25017  mule1  25411  ppiub  25466  dchrabs2  25524  bposlem1  25546  zabsle1  25558  lgseisen  25641  lgsquadlem2  25643  rpvmasumlem  25749  qabvle  25887  ostth3  25900  colinearalg  26383  eengstr  26453  clwwlknon1le1  27566  eucrct2eupth  27710  nmosetn0  28229  nmoo0  28255  siii  28317  bcsiALT  28643  branmfn  29569  esumrnmpt2  30940  ballotlemrc  31401  pthhashvtx  31984  subfacval3  32046  sconnpi1  32096  fz0n  32572  poimirlem31  34475  itg2addnclem  34495  ftc1anc  34527  radcnvrat  40205  infxr  41197  stoweidlem18  41867  stoweidlem55  41904  fourierdlem62  42017  fourierswlem  42079  exple2lt6  43914