Theorem sseqtrdi 4004

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3948

This theorem is referenced by:  sseqtrrdi  4005  3sstr3g  4016  sofld  6187  relrelss  6273  foimacnv  6845  onfununi  8363  hartogslem1  9564  cantnfp1lem3  9702  uniwf  9841  rankeq0b  9882  djuinf  10211  cflecard  10275  fin23lem16  10357  fin23lem41  10374  pwcfsdom  10605  fpwwe2lem12  10664  fpwwe2  10665  canth4  10669  hashbclem  14473  dmtrclfv  15039  zsum  15736  fsumcvg3  15747  incexclem  15854  zprod  15955  ramub1lem1  17046  setsstruct2  17193  imasaddfnlem  17544  imasvscafn  17553  mremre  17618  submre  17619  mreexexlem3d  17660  isacs1i  17671  acsmapd  18568  acsmap2d  18569  ghmqusnsglem1  19267  gsumzoppg  19930  rhmimasubrnglem  20533  subdrgint  20772  primefld  20774  lspsntri  21064  lsppratlem4  21120  lbsextlem3  21130  sraring  21155  evls1maplmhm  22329  distop  22949  elcls  23027  cnpresti  23242  cnprest  23243  cmpcld  23356  cnconn  23376  iunconn  23382  comppfsc  23486  ptuni2  23530  alexsubALTlem3  24003  ustssco  24169  ust0  24174  ustbas2  24180  ustimasn  24183  utopbas  24190  utop2nei  24205  setsmstopn  24435  metustsym  24512  metust  24515  tngtopn  24607  ovoliunlem1  25473  lhop1lem  25988  ig1peu  26150  ig1pdvds  26155  logccv  26641  amgmlem  26969  upgr1e  29058  uspgr1e  29189  shsupcl  31285  shsupunss  31293  shslubi  31332  orthin  31393  h1datomi  31528  mdslj2i  32267  mdslmd1lem1  32272  iundifdifd  32509  iunxpssiun1  32516  difres  32548  fresf1o  32576  suppovss  32625  swrdrndisj  32882  elrgspnlem3  33187  fracf1  33249  idomsubr  33251  nsgmgclem  33374  sradrng  33568  sraidom  33569  resssra  33573  lsssra  33574  zarcmplem  33839  metideq  33851  hauseqcn  33856  tpr2rico  33870  esumrnmpt2  34028  esumpfinvallem  34034  esum2d  34053  omssubadd  34261  carsggect  34279  omsmeas  34284  orvcelval  34430  signsply0  34525  cvmlift2lem11  35277  cvmlift2lem12  35278  dfon2lem7  35749  filnetlem3  36340  onsucsuccmpi  36403  dissneqlem  37300  icoreunrn  37319  ctbssinf  37366  pibt2  37377  mblfinlem1  37623  ismblfin  37627  sstotbnd2  37740  dochexmidlem4  41424  lcfrlem38  41541  rhmqusspan  42145  mhpind  42567  ismrcd1  42672  eldioph2lem2  42735  rmxyelqirrOLD  42885  hbt  43105  rngunsnply  43144  iocinico  43187  dmtrcl  43602  rntrcl  43603  trrelsuperrel2dg  43646  restuni5  45085  unirnmapsn  45176  limciccioolb  45593  limcrecl  45601  limcicciooub  45609  stoweidlem50  46022  stoweidlem52  46024  stoweidlem53  46025  stoweidlem57  46029  stoweidlem59  46031  fourierdlem50  46128  fourierdlem103  46181  fourierdlem104  46182  pwsal  46287  sge0iun  46391  sge0isum  46399  meadjuni  46429  omessle  46470  zlmodzxzel  48229  lincresunit3  48356  amgmwlem  49329