Theorem sseqtrdi 3978

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  sseqtrrdi  3979  3sstr3g  3990  sofld  6187  relrelss  6276  foimacnv  6840  onfununi  8329  hartogslem1  9505  cantnfp1lem3  9650  uniwf  9792  rankeq0b  9833  djuinf  10173  cflecard  10237  fin23lem16  10320  fin23lem41  10337  pwcfsdom  10569  fpwwe2lem12  10628  fpwwe2  10629  canth4  10633  hashbclem  14491  dmtrclfv  15057  zsum  15771  fsumcvg3  15782  incexclem  15892  zprod  15993  ramub1lem1  17087  setsstruct2  17235  imasaddfnlem  17583  imasvscafn  17592  mremre  17657  submre  17658  mreexexlem3d  17703  isacs1i  17714  acsmapd  18611  acsmap2d  18612  ghmqusnsglem1  19351  gsumzoppg  20015  rhmimasubrnglem  20651  subdrgint  20887  primefld  20889  lspsntri  21199  lsppratlem4  21255  lbsextlem3  21265  sraring  21288  evls1maplmhm  22518  distop  23133  elcls  23211  cnpresti  23426  cnprest  23427  cmpcld  23540  cnconn  23560  iunconn  23566  comppfsc  23670  ptuni2  23714  alexsubALTlem3  24187  ustssco  24353  ust0  24358  ustbas2  24363  ustimasn  24366  utopbas  24373  utop2nei  24388  setsmstopn  24616  metustsym  24693  metust  24696  tngtopn  24788  ovoliunlem1  25642  lhop1lem  26153  ig1peu  26313  ig1pdvds  26318  logccv  26809  amgmlem  27135  upgr1e  29444  uspgr1e  29575  shsupcl  31671  shsupunss  31679  shslubi  31718  orthin  31779  h1datomi  31914  mdslj2i  32653  mdslmd1lem1  32658  iundifdifd  32887  iunxpssiun1  32894  difres  32926  fresf1o  32957  suppovss  33007  swrdrndisj  33258  elrgspnlem3  33545  fracf1  33609  idomsubr  33611  nsgmgclem  33701  ressply1evls1  33836  sradrng  33953  sraidom  33954  resssra  33958  lsssra  33959  extdgfialglem1  34063  extdgfialglem2  34064  zarcmplem  34252  metideq  34264  hauseqcn  34269  tpr2rico  34283  esumrnmpt2  34439  esumpfinvallem  34445  esum2d  34464  omssubadd  34671  carsggect  34689  omsmeas  34694  orvcelval  34840  signsply0  34919  cvmlift2lem11  35786  cvmlift2lem12  35787  dfon2lem7  36260  filnetlem3  36872  onsucsuccmpi  36935  dissneqlem  37967  icoreunrn  37986  ctbssinf  38033  pibt2  38044  mblfinlem1  38289  ismblfin  38293  sstotbnd2  38406  dochexmidlem4  42218  lcfrlem38  42335  rhmqusspan  42933  mhpind  43309  ismrcd1  43412  eldioph2lem2  43475  hbt  43840  rngunsnply  43879  iocinico  43922  dmtrcl  44336  rntrcl  44337  trrelsuperrel2dg  44380  restuni5  45824  unirnmapsn  45913  limciccioolb  46320  limcrecl  46328  limcicciooub  46334  stoweidlem50  46747  stoweidlem52  46749  stoweidlem53  46750  stoweidlem57  46754  stoweidlem59  46756  fourierdlem50  46853  fourierdlem103  46906  fourierdlem104  46907  pwsal  47012  sge0iun  47116  sge0isum  47124  meadjuni  47154  omessle  47195  uhgrimprop  48640  zlmodzxzel  49118  lincresunit3  49244  amgmwlem  50585