Theorem syl6sseq 3938

Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
syl6sseq.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
syl6sseq.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
syl6sseq	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem syl6sseq

Step	Hyp	Ref	Expression
1		syl6sseq.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		syl6sseq.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	sseq2i 3917	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶)
4	1, 3	sylib 219	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1522   ⊆ wss 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-in 3866  df-ss 3874

This theorem is referenced by:  syl6sseqr  3939  sofld  5920  relrelss  5999  foimacnv  6500  onfununi  7830  hartogslem1  8852  cantnfp1lem3  8989  uniwf  9094  rankeq0b  9135  djuinf  9460  cflecard  9521  fin23lem16  9603  fin23lem41  9620  pwcfsdom  9851  fpwwe2lem13  9910  fpwwe2  9911  canth4  9915  hashbclem  13658  dmtrclfv  14212  zsum  14908  fsumcvg3  14919  incexclem  15024  zprod  15124  ramub1lem1  16191  setsstruct2  16350  imasaddfnlem  16630  imasvscafn  16639  mremre  16704  submre  16705  mreexexlem3d  16746  isacs1i  16757  acsmapd  17617  acsmap2d  17618  gsumzoppg  18784  subdrgint  19272  primefld  19274  lspsntri  19559  lsppratlem4  19612  lbsextlem3  19622  distop  21287  elcls  21365  cnpresti  21580  cnprest  21581  cmpcld  21694  cnconn  21714  iunconn  21720  comppfsc  21824  ptuni2  21868  alexsubALTlem3  22341  ustssco  22506  ust0  22511  ustbas2  22517  ustimasn  22520  utopbas  22527  utop2nei  22542  setsmstopn  22771  metustsym  22848  metust  22851  tngtopn  22942  ovoliunlem1  23786  lhop1lem  24293  ig1peu  24448  ig1pdvds  24453  logccv  24927  amgmlem  25249  upgr1e  26581  uspgr1e  26709  shsupcl  28806  shsupunss  28814  shslubi  28853  orthin  28914  h1datomi  29049  mdslj2i  29788  mdslmd1lem1  29793  pwuniss  29995  iundifdifd  30003  difres  30040  fresf1o  30066  suppovss  30116  sraring  30591  sradrng  30592  metideq  30750  hauseqcn  30755  tpr2rico  30772  esumrnmpt2  30944  esumpfinvallem  30950  esum2d  30969  omssubadd  31175  carsggect  31193  omsmeas  31198  orvcelval  31343  signsply0  31438  cvmlift2lem11  32169  cvmlift2lem12  32170  dfon2lem7  32643  filnetlem3  33338  onsucsuccmpi  33401  dissneqlem  34171  icoreunrn  34190  ctbssinf  34237  pibt2  34248  mblfinlem1  34479  ismblfin  34483  sstotbnd2  34603  dochexmidlem4  38149  lcfrlem38  38266  ismrcd1  38799  eldioph2lem2  38862  rmxyelqirr  39011  hbt  39234  rngunsnply  39277  iocinico  39322  dmtrcl  39491  rntrcl  39492  trrelsuperrel2dg  39520  restuni5  40948  unirnmapsn  41036  limciccioolb  41463  limcrecl  41471  limcicciooub  41479  stoweidlem50  41897  stoweidlem52  41899  stoweidlem53  41900  stoweidlem57  41904  stoweidlem59  41906  fourierdlem50  42003  fourierdlem103  42056  fourierdlem104  42057  pwsal  42162  sge0iun  42263  sge0isum  42271  meadjuni  42301  omessle  42342  zlmodzxzel  43901  lincresunit3  44036  amgmwlem  44403