Theorem sseqtrdi 3962

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

Hypotheses

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

Assertion

Ref	Expression
sseqtrdi	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrdi

Step	Hyp	Ref	Expression
1		sseqtrdi.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrdi.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	sseq2i 3951	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶)
4	1, 3	sylib 218	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  sseqtrrdi  3963  3sstr3g  3974  sofld  6151  relrelss  6237  foimacnv  6797  onfununi  8281  hartogslem1  9457  cantnfp1lem3  9601  uniwf  9743  rankeq0b  9784  djuinf  10111  cflecard  10175  fin23lem16  10257  fin23lem41  10274  pwcfsdom  10506  fpwwe2lem12  10565  fpwwe2  10566  canth4  10570  hashbclem  14414  dmtrclfv  14980  zsum  15680  fsumcvg3  15691  incexclem  15801  zprod  15902  ramub1lem1  16997  setsstruct2  17144  imasaddfnlem  17492  imasvscafn  17501  mremre  17566  submre  17567  mreexexlem3d  17612  isacs1i  17623  acsmapd  18520  acsmap2d  18521  ghmqusnsglem1  19255  gsumzoppg  19919  rhmimasubrnglem  20542  subdrgint  20780  primefld  20782  lspsntri  21092  lsppratlem4  21148  lbsextlem3  21158  sraring  21181  evls1maplmhm  22342  distop  22960  elcls  23038  cnpresti  23253  cnprest  23254  cmpcld  23367  cnconn  23387  iunconn  23393  comppfsc  23497  ptuni2  23541  alexsubALTlem3  24014  ustssco  24180  ust0  24185  ustbas2  24190  ustimasn  24193  utopbas  24200  utop2nei  24215  setsmstopn  24443  metustsym  24520  metust  24523  tngtopn  24615  ovoliunlem1  25469  lhop1lem  25980  ig1peu  26140  ig1pdvds  26145  logccv  26627  amgmlem  26953  upgr1e  29182  uspgr1e  29313  shsupcl  31409  shsupunss  31417  shslubi  31456  orthin  31517  h1datomi  31652  mdslj2i  32391  mdslmd1lem1  32396  iundifdifd  32631  iunxpssiun1  32638  difres  32670  fresf1o  32704  suppovss  32754  swrdrndisj  33017  elrgspnlem3  33305  fracf1  33368  idomsubr  33370  nsgmgclem  33471  ressply1evls1  33625  sradrng  33726  sraidom  33727  resssra  33731  lsssra  33732  extdgfialglem1  33836  extdgfialglem2  33837  zarcmplem  34025  metideq  34037  hauseqcn  34042  tpr2rico  34056  esumrnmpt2  34212  esumpfinvallem  34218  esum2d  34237  omssubadd  34444  carsggect  34462  omsmeas  34467  orvcelval  34613  signsply0  34695  cvmlift2lem11  35495  cvmlift2lem12  35496  dfon2lem7  35969  filnetlem3  36562  onsucsuccmpi  36625  dissneqlem  37656  icoreunrn  37675  ctbssinf  37722  pibt2  37733  mblfinlem1  37978  ismblfin  37982  sstotbnd2  38095  dochexmidlem4  41909  lcfrlem38  42026  rhmqusspan  42624  mhpind  43027  ismrcd1  43130  eldioph2lem2  43193  hbt  43558  rngunsnply  43597  iocinico  43640  dmtrcl  44054  rntrcl  44055  trrelsuperrel2dg  44098  restuni5  45553  unirnmapsn  45643  limciccioolb  46051  limcrecl  46059  limcicciooub  46065  stoweidlem50  46478  stoweidlem52  46480  stoweidlem53  46481  stoweidlem57  46485  stoweidlem59  46487  fourierdlem50  46584  fourierdlem103  46637  fourierdlem104  46638  pwsal  46743  sge0iun  46847  sge0isum  46855  meadjuni  46885  omessle  46926  uhgrimprop  48368  zlmodzxzel  48831  lincresunit3  48957  amgmwlem  50277