Theorem syl6eqbr 4692

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

Syntax hints:   → wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  syl6eqbrr  4693  domunsn  8110  mapdom1  8125  mapdom2  8131  pm54.43  8826  cdadom1  9008  infmap2  9040  inar1  9597  gruina  9640  nn0ledivnn  11941  xltnegi  12047  leexp1a  12919  discr  13001  facwordi  13076  faclbnd3  13079  hashgt12el  13210  hashle2pr  13259  cnpart  13980  geomulcvg  14607  dvds1  15041  ramz2  15728  ramz  15729  gex1  18006  sylow2a  18034  en1top  20788  en2top  20789  hmph0  21598  ptcmplem2  21857  dscmet  22377  dscopn  22378  xrge0tsms2  22638  htpycc  22779  pcohtpylem  22819  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevlem  22826  vitalilem5  23381  dvef  23743  dveq0  23763  dv11cn  23764  deg1lt0  23851  ply1rem  23923  fta1g  23927  plyremlem  24059  aalioulem3  24089  pige3  24269  relogrn  24308  logneg  24334  cxpaddlelem  24492  mule1  24874  ppiub  24929  dchrabs2  24987  bposlem1  25009  zabsle1  25021  lgseisen  25104  lgsquadlem2  25106  rpvmasumlem  25176  qabvle  25314  ostth3  25327  colinearalg  25790  eengstr  25860  eucrct2eupth  27105  nmosetn0  27620  nmoo0  27646  siii  27708  bcsiALT  28036  branmfn  28964  esumrnmpt2  30130  ballotlemrc  30592  subfacval3  31171  sconnpi1  31221  fz0n  31616  poimirlem31  33440  itg2addnclem  33461  ftc1anc  33493  radcnvrat  38513  infxr  39583  stoweidlem18  40235  stoweidlem55  40272  fourierdlem62  40385  fourierswlem  40447  exple2lt6  42145