Theorem sseqtrdi 4030

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

Syntax hints:   → wi 4   = wceq 1534   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  sseqtrrdi  4031  sofld  6191  relrelss  6277  foimacnv  6856  onfununi  8361  hartogslem1  9565  cantnfp1lem3  9703  uniwf  9842  rankeq0b  9883  djuinf  10211  cflecard  10276  fin23lem16  10358  fin23lem41  10375  pwcfsdom  10606  fpwwe2lem12  10665  fpwwe2  10666  canth4  10670  hashbclem  14443  dmtrclfv  14997  zsum  15696  fsumcvg3  15707  incexclem  15814  zprod  15913  ramub1lem1  16994  setsstruct2  17142  imasaddfnlem  17509  imasvscafn  17518  mremre  17583  submre  17584  mreexexlem3d  17625  isacs1i  17636  acsmapd  18545  acsmap2d  18546  gsumzoppg  19898  rhmimasubrnglem  20501  subdrgint  20690  primefld  20692  lspsntri  20981  lsppratlem4  21037  lbsextlem3  21047  sraring  21078  distop  22897  elcls  22976  cnpresti  23191  cnprest  23192  cmpcld  23305  cnconn  23325  iunconn  23331  comppfsc  23435  ptuni2  23479  alexsubALTlem3  23952  ustssco  24118  ust0  24123  ustbas2  24129  ustimasn  24132  utopbas  24139  utop2nei  24154  setsmstopn  24385  metustsym  24463  metust  24466  tngtopn  24566  ovoliunlem1  25430  lhop1lem  25945  ig1peu  26108  ig1pdvds  26113  logccv  26596  amgmlem  26921  upgr1e  28925  uspgr1e  29056  shsupcl  31147  shsupunss  31155  shslubi  31194  orthin  31255  h1datomi  31390  mdslj2i  32129  mdslmd1lem1  32134  iundifdifd  32351  difres  32389  fresf1o  32415  suppovss  32464  swrdrndisj  32678  fracf1  32993  idomsubr  32995  nsgmgclem  33121  ghmqusnsglem1  33129  sradrng  33279  resssra  33283  lsssra  33284  evls1maplmhm  33370  zarcmplem  33482  metideq  33494  hauseqcn  33499  tpr2rico  33513  esumrnmpt2  33687  esumpfinvallem  33693  esum2d  33712  omssubadd  33920  carsggect  33938  omsmeas  33943  orvcelval  34088  signsply0  34183  cvmlift2lem11  34923  cvmlift2lem12  34924  dfon2lem7  35385  filnetlem3  35864  onsucsuccmpi  35927  dissneqlem  36819  icoreunrn  36838  ctbssinf  36885  pibt2  36896  mblfinlem1  37130  ismblfin  37134  sstotbnd2  37247  dochexmidlem4  40936  lcfrlem38  41053  mhpind  41827  ismrcd1  42118  eldioph2lem2  42181  rmxyelqirrOLD  42331  hbt  42554  rngunsnply  42597  iocinico  42640  dmtrcl  43057  rntrcl  43058  trrelsuperrel2dg  43101  restuni5  44489  unirnmapsn  44587  limciccioolb  45009  limcrecl  45017  limcicciooub  45025  stoweidlem50  45438  stoweidlem52  45440  stoweidlem53  45441  stoweidlem57  45445  stoweidlem59  45447  fourierdlem50  45544  fourierdlem103  45597  fourierdlem104  45598  pwsal  45703  sge0iun  45807  sge0isum  45815  meadjuni  45845  omessle  45886  zlmodzxzel  47419  lincresunit3  47549  amgmwlem  48235