Theorem syl6eqbr 4616

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

Syntax hints:   → wi 4   = wceq 1474   class class class wbr 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578

This theorem is referenced by:  syl6eqbrr  4617  domunsn  7972  mapdom1  7987  mapdom2  7993  pm54.43  8686  cdadom1  8868  infmap2  8900  inar1  9453  gruina  9496  nn0ledivnn  11775  xltnegi  11882  leexp1a  12738  discr  12820  facwordi  12895  faclbnd3  12898  hashgt12el  13024  cnpart  13776  geomulcvg  14394  dvds1  14827  ramz2  15514  ramz  15515  gex1  17777  sylow2a  17805  en1top  20546  en2top  20547  hmph0  21355  ptcmplem2  21614  dscmet  22134  dscopn  22135  xrge0tsms2  22393  htpycc  22534  pcohtpylem  22574  pcopt  22577  pcopt2  22578  pcoass  22579  pcorevlem  22581  vitalilem5  23131  dvef  23491  dveq0  23511  dv11cn  23512  deg1lt0  23599  ply1rem  23671  fta1g  23675  plyremlem  23807  aalioulem3  23837  pige3  24017  relogrn  24056  logneg  24082  cxpaddlelem  24236  mule1  24618  ppiub  24673  dchrabs2  24731  bposlem1  24753  zabsle1  24765  lgseisen  24848  lgsquadlem2  24850  rpvmasumlem  24920  qabvle  25058  ostth3  25071  colinearalg  25535  eengstr  25605  konigsberg  26307  nmosetn0  26797  nmoo0  26823  siii  26885  bcsiALT  27213  branmfn  28141  esumrnmpt2  29250  ballotlemrc  29712  subfacval3  30218  sconpi1  30268  fz0n  30662  poimirlem31  32393  itg2addnclem  32414  ftc1anc  32446  radcnvrat  37318  infxr  38307  stoweidlem18  38694  stoweidlem55  38731  fourierdlem62  38844  fourierswlem  38906  eucrct2eupth  41394  exple2lt6  41920