Theorem syl6sseq 3614

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 3593	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶)
4	1, 3	sylib 207	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  syl6sseqr  3615  sofld  5500  relrelss  5576  foimacnv  6067  onfununi  7325  hartogslem1  8330  cantnfp1lem3  8460  uniwf  8565  rankeq0b  8606  cflecard  8958  fin23lem16  9040  fin23lem41  9057  pwcfsdom  9284  fpwwe2lem13  9343  fpwwe2  9344  canth4  9348  hashbclem  13093  dmtrclfv  13607  zsum  14296  fsumcvg3  14307  incexclem  14407  zprod  14506  ramub1lem1  15568  imasaddfnlem  16011  imasvscafn  16020  mremre  16087  submre  16088  mreexexlem3d  16129  isacs1i  16141  acsmapd  17001  acsmap2d  17002  gsumzoppg  18167  lspsntri  18918  lsppratlem4  18971  lbsextlem3  18981  distop  20610  elcls  20687  cnpresti  20902  cnprest  20903  cmpcld  21015  cnconn  21035  iuncon  21041  comppfsc  21145  ptuni2  21189  alexsubALTlem3  21663  ustssco  21828  ust0  21833  ustbas2  21839  ustimasn  21842  utopbas  21849  utop2nei  21864  setsmstopn  22093  metustsym  22170  metust  22173  tngtopn  22264  ovoliunlem1  23077  lhop1lem  23580  ig1peu  23735  ig1pdvds  23740  logccv  24209  amgmlem  24516  upgr1e  25779  shsupcl  27581  shsupunss  27589  shslubi  27628  orthin  27689  h1datomi  27824  mdslj2i  28563  mdslmd1lem1  28568  pwuniss  28753  iundifdifd  28762  difres  28795  fresf1o  28815  metideq  29264  hauseqcn  29269  tpr2rico  29286  esumrnmpt2  29457  esumpfinvallem  29463  esum2d  29482  omssubadd  29689  carsggect  29707  omsmeas  29712  orvcelval  29857  signsply0  29954  cvmlift2lem11  30549  cvmlift2lem12  30550  dfon2lem7  30938  filnetlem3  31545  onsucsuccmpi  31612  dissneqlem  32363  icoreunrn  32383  mblfinlem1  32616  ismblfin  32620  sstotbnd2  32743  dochexmidlem4  35770  lcfrlem38  35887  ismrcd1  36279  eldioph2lem2  36342  rmxyelqirr  36493  hbt  36719  rngunsnply  36762  iocinico  36816  dmtrcl  36953  rntrcl  36954  trrelsuperrel2dg  36982  restuni5  38338  unirnmapsn  38401  limciccioolb  38688  limcrecl  38696  limcicciooub  38704  stoweidlem50  38943  stoweidlem52  38945  stoweidlem53  38946  stoweidlem57  38950  stoweidlem59  38952  fourierdlem50  39049  fourierdlem103  39102  fourierdlem104  39103  pwsal  39211  sge0iun  39312  sge0isum  39320  meadjuni  39350  omessle  39388  uspgr1e  40470  zlmodzxzel  41926  lincresunit3  42064  amgmwlem  42357