Theorem syl6eqbr 4843

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

Syntax hints:   → wi 4   = wceq 1632   class class class wbr 4804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805

This theorem is referenced by:  syl6eqbrr  4844  domunsn  8277  mapdom1  8292  mapdom2  8298  pm54.43  9036  cdadom1  9220  infmap2  9252  inar1  9809  gruina  9852  nn0ledivnn  12154  xltnegi  12260  leexp1a  13133  discr  13215  facwordi  13290  faclbnd3  13293  hashgt12el  13422  hashle2pr  13471  cnpart  14199  geomulcvg  14826  dvds1  15263  ramz2  15950  ramz  15951  gex1  18226  sylow2a  18254  en1top  21010  en2top  21011  hmph0  21820  ptcmplem2  22078  dscmet  22598  dscopn  22599  xrge0tsms2  22859  htpycc  23000  pcohtpylem  23039  pcopt  23042  pcopt2  23043  pcoass  23044  pcorevlem  23046  vitalilem5  23600  dvef  23962  dveq0  23982  dv11cn  23983  deg1lt0  24070  ply1rem  24142  fta1g  24146  plyremlem  24278  aalioulem3  24308  pige3  24489  relogrn  24528  logneg  24554  cxpaddlelem  24712  mule1  25094  ppiub  25149  dchrabs2  25207  bposlem1  25229  zabsle1  25241  lgseisen  25324  lgsquadlem2  25326  rpvmasumlem  25396  qabvle  25534  ostth3  25547  colinearalg  26010  eengstr  26080  clwwlknon1le1  27270  eucrct2eupth  27418  nmosetn0  27950  nmoo0  27976  siii  28038  bcsiALT  28366  branmfn  29294  esumrnmpt2  30460  ballotlemrc  30922  subfacval3  31499  sconnpi1  31549  fz0n  31944  poimirlem31  33771  itg2addnclem  33792  ftc1anc  33824  radcnvrat  39033  infxr  40099  stoweidlem18  40756  stoweidlem55  40793  fourierdlem62  40906  fourierswlem  40968  exple2lt6  42673