Theorem sseqtrdi 4027

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-v 3470  df-in 3950  df-ss 3960

This theorem is referenced by:  sseqtrrdi  4028  sofld  6180  relrelss  6266  foimacnv  6844  onfununi  8342  hartogslem1  9539  cantnfp1lem3  9677  uniwf  9816  rankeq0b  9857  djuinf  10185  cflecard  10250  fin23lem16  10332  fin23lem41  10349  pwcfsdom  10580  fpwwe2lem12  10639  fpwwe2  10640  canth4  10644  hashbclem  14417  dmtrclfv  14971  zsum  15670  fsumcvg3  15681  incexclem  15788  zprod  15887  ramub1lem1  16968  setsstruct2  17116  imasaddfnlem  17483  imasvscafn  17492  mremre  17557  submre  17558  mreexexlem3d  17599  isacs1i  17610  acsmapd  18519  acsmap2d  18520  gsumzoppg  19864  rhmimasubrnglem  20465  subdrgint  20654  primefld  20656  lspsntri  20945  lsppratlem4  21001  lbsextlem3  21011  sraring  21042  distop  22853  elcls  22932  cnpresti  23147  cnprest  23148  cmpcld  23261  cnconn  23281  iunconn  23287  comppfsc  23391  ptuni2  23435  alexsubALTlem3  23908  ustssco  24074  ust0  24079  ustbas2  24085  ustimasn  24088  utopbas  24095  utop2nei  24110  setsmstopn  24341  metustsym  24419  metust  24422  tngtopn  24522  ovoliunlem1  25386  lhop1lem  25901  ig1peu  26064  ig1pdvds  26069  logccv  26552  amgmlem  26877  upgr1e  28881  uspgr1e  29009  shsupcl  31100  shsupunss  31108  shslubi  31147  orthin  31208  h1datomi  31343  mdslj2i  32082  mdslmd1lem1  32087  iundifdifd  32302  difres  32340  fresf1o  32364  suppovss  32413  swrdrndisj  32626  nsgmgclem  33028  sradrng  33188  resssra  33192  lsssra  33193  evls1maplmhm  33279  zarcmplem  33391  metideq  33403  hauseqcn  33408  tpr2rico  33422  esumrnmpt2  33596  esumpfinvallem  33602  esum2d  33621  omssubadd  33829  carsggect  33847  omsmeas  33852  orvcelval  33997  signsply0  34092  cvmlift2lem11  34832  cvmlift2lem12  34833  dfon2lem7  35294  filnetlem3  35773  onsucsuccmpi  35836  dissneqlem  36728  icoreunrn  36747  ctbssinf  36794  pibt2  36805  mblfinlem1  37038  ismblfin  37042  sstotbnd2  37155  dochexmidlem4  40847  lcfrlem38  40964  mhpind  41723  ismrcd1  42014  eldioph2lem2  42077  rmxyelqirrOLD  42227  hbt  42450  rngunsnply  42493  iocinico  42537  dmtrcl  42954  rntrcl  42955  trrelsuperrel2dg  42998  restuni5  44387  unirnmapsn  44485  limciccioolb  44909  limcrecl  44917  limcicciooub  44925  stoweidlem50  45338  stoweidlem52  45340  stoweidlem53  45341  stoweidlem57  45345  stoweidlem59  45347  fourierdlem50  45444  fourierdlem103  45497  fourierdlem104  45498  pwsal  45603  sge0iun  45707  sge0isum  45715  meadjuni  45745  omessle  45786  zlmodzxzel  47307  lincresunit3  47437  amgmwlem  48123