Theorem sseqtrdi 3967

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sseqtrrdi  3968  sofld  6079  relrelss  6165  foimacnv  6717  onfununi  8143  hartogslem1  9231  cantnfp1lem3  9368  uniwf  9508  rankeq0b  9549  djuinf  9875  cflecard  9940  fin23lem16  10022  fin23lem41  10039  pwcfsdom  10270  fpwwe2lem12  10329  fpwwe2  10330  canth4  10334  hashbclem  14092  dmtrclfv  14657  zsum  15358  fsumcvg3  15369  incexclem  15476  zprod  15575  ramub1lem1  16655  setsstruct2  16803  imasaddfnlem  17156  imasvscafn  17165  mremre  17230  submre  17231  mreexexlem3d  17272  isacs1i  17283  acsmapd  18187  acsmap2d  18188  gsumzoppg  19460  subdrgint  19986  primefld  19988  lspsntri  20274  lsppratlem4  20327  lbsextlem3  20337  distop  22053  elcls  22132  cnpresti  22347  cnprest  22348  cmpcld  22461  cnconn  22481  iunconn  22487  comppfsc  22591  ptuni2  22635  alexsubALTlem3  23108  ustssco  23274  ust0  23279  ustbas2  23285  ustimasn  23288  utopbas  23295  utop2nei  23310  setsmstopn  23539  metustsym  23617  metust  23620  tngtopn  23720  ovoliunlem1  24571  lhop1lem  25082  ig1peu  25241  ig1pdvds  25246  logccv  25723  amgmlem  26044  upgr1e  27386  uspgr1e  27514  shsupcl  29601  shsupunss  29609  shslubi  29648  orthin  29709  h1datomi  29844  mdslj2i  30583  mdslmd1lem1  30588  iundifdifd  30802  difres  30840  fresf1o  30867  suppovss  30919  swrdrndisj  31131  nsgmgclem  31498  sraring  31574  sradrng  31575  zarcmplem  31733  metideq  31745  hauseqcn  31750  tpr2rico  31764  esumrnmpt2  31936  esumpfinvallem  31942  esum2d  31961  omssubadd  32167  carsggect  32185  omsmeas  32190  orvcelval  32335  signsply0  32430  cvmlift2lem11  33175  cvmlift2lem12  33176  dfon2lem7  33671  filnetlem3  34496  onsucsuccmpi  34559  dissneqlem  35438  icoreunrn  35457  ctbssinf  35504  pibt2  35515  mblfinlem1  35741  ismblfin  35745  sstotbnd2  35859  dochexmidlem4  39404  lcfrlem38  39521  mhpind  40206  ismrcd1  40436  eldioph2lem2  40499  rmxyelqirr  40648  hbt  40871  rngunsnply  40914  iocinico  40959  dmtrcl  41124  rntrcl  41125  trrelsuperrel2dg  41168  restuni5  42561  unirnmapsn  42643  limciccioolb  43052  limcrecl  43060  limcicciooub  43068  stoweidlem50  43481  stoweidlem52  43483  stoweidlem53  43484  stoweidlem57  43488  stoweidlem59  43490  fourierdlem50  43587  fourierdlem103  43640  fourierdlem104  43641  pwsal  43746  sge0iun  43847  sge0isum  43855  meadjuni  43885  omessle  43926  zlmodzxzel  45579  lincresunit3  45710  amgmwlem  46392