Theorem sseqtrdi 3976

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

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

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 2709

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

This theorem is referenced by:  sseqtrrdi  3977  3sstr3g  3988  sofld  6153  relrelss  6239  foimacnv  6799  onfununi  8283  hartogslem1  9459  cantnfp1lem3  9601  uniwf  9743  rankeq0b  9784  djuinf  10111  cflecard  10175  fin23lem16  10257  fin23lem41  10274  pwcfsdom  10506  fpwwe2lem12  10565  fpwwe2  10566  canth4  10570  hashbclem  14387  dmtrclfv  14953  zsum  15653  fsumcvg3  15664  incexclem  15771  zprod  15872  ramub1lem1  16966  setsstruct2  17113  imasaddfnlem  17461  imasvscafn  17470  mremre  17535  submre  17536  mreexexlem3d  17581  isacs1i  17592  acsmapd  18489  acsmap2d  18490  ghmqusnsglem1  19221  gsumzoppg  19885  rhmimasubrnglem  20510  subdrgint  20748  primefld  20750  lspsntri  21061  lsppratlem4  21117  lbsextlem3  21127  sraring  21150  evls1maplmhm  22333  distop  22951  elcls  23029  cnpresti  23244  cnprest  23245  cmpcld  23358  cnconn  23378  iunconn  23384  comppfsc  23488  ptuni2  23532  alexsubALTlem3  24005  ustssco  24171  ust0  24176  ustbas2  24181  ustimasn  24184  utopbas  24191  utop2nei  24206  setsmstopn  24434  metustsym  24511  metust  24514  tngtopn  24606  ovoliunlem1  25471  lhop1lem  25986  ig1peu  26148  ig1pdvds  26153  logccv  26640  amgmlem  26968  upgr1e  29198  uspgr1e  29329  shsupcl  31425  shsupunss  31433  shslubi  31472  orthin  31533  h1datomi  31668  mdslj2i  32407  mdslmd1lem1  32412  iundifdifd  32647  iunxpssiun1  32654  difres  32686  fresf1o  32720  suppovss  32770  swrdrndisj  33049  elrgspnlem3  33337  fracf1  33400  idomsubr  33402  nsgmgclem  33503  ressply1evls1  33657  sradrng  33758  sraidom  33759  resssra  33763  lsssra  33764  extdgfialglem1  33869  extdgfialglem2  33870  zarcmplem  34058  metideq  34070  hauseqcn  34075  tpr2rico  34089  esumrnmpt2  34245  esumpfinvallem  34251  esum2d  34270  omssubadd  34477  carsggect  34495  omsmeas  34500  orvcelval  34646  signsply0  34728  cvmlift2lem11  35526  cvmlift2lem12  35527  dfon2lem7  36000  filnetlem3  36593  onsucsuccmpi  36656  dissneqlem  37589  icoreunrn  37608  ctbssinf  37655  pibt2  37666  mblfinlem1  37902  ismblfin  37906  sstotbnd2  38019  dochexmidlem4  41833  lcfrlem38  41950  rhmqusspan  42549  mhpind  42946  ismrcd1  43049  eldioph2lem2  43112  hbt  43481  rngunsnply  43520  iocinico  43563  dmtrcl  43977  rntrcl  43978  trrelsuperrel2dg  44021  restuni5  45476  unirnmapsn  45566  limciccioolb  45975  limcrecl  45983  limcicciooub  45989  stoweidlem50  46402  stoweidlem52  46404  stoweidlem53  46405  stoweidlem57  46409  stoweidlem59  46411  fourierdlem50  46508  fourierdlem103  46561  fourierdlem104  46562  pwsal  46667  sge0iun  46771  sge0isum  46779  meadjuni  46809  omessle  46850  uhgrimprop  48246  zlmodzxzel  48709  lincresunit3  48835  amgmwlem  50155