Theorem sseqtrdi 4032

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  sseqtrrdi  4033  sofld  6186  relrelss  6272  foimacnv  6850  onfununi  8343  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  14413  dmtrclfv  14967  zsum  15666  fsumcvg3  15677  incexclem  15784  zprod  15883  ramub1lem1  16961  setsstruct2  17109  imasaddfnlem  17476  imasvscafn  17485  mremre  17550  submre  17551  mreexexlem3d  17592  isacs1i  17603  acsmapd  18509  acsmap2d  18510  gsumzoppg  19814  subdrgint  20423  primefld  20425  lspsntri  20713  lsppratlem4  20769  lbsextlem3  20779  sraring  20814  distop  22505  elcls  22584  cnpresti  22799  cnprest  22800  cmpcld  22913  cnconn  22933  iunconn  22939  comppfsc  23043  ptuni2  23087  alexsubALTlem3  23560  ustssco  23726  ust0  23731  ustbas2  23737  ustimasn  23740  utopbas  23747  utop2nei  23762  setsmstopn  23993  metustsym  24071  metust  24074  tngtopn  24174  ovoliunlem1  25026  lhop1lem  25537  ig1peu  25696  ig1pdvds  25701  logccv  26178  amgmlem  26501  upgr1e  28411  uspgr1e  28539  shsupcl  30629  shsupunss  30637  shslubi  30676  orthin  30737  h1datomi  30872  mdslj2i  31611  mdslmd1lem1  31616  iundifdifd  31831  difres  31869  fresf1o  31893  suppovss  31944  swrdrndisj  32159  nsgmgclem  32567  sradrng  32729  resssra  32733  lsssra  32734  evls1maplmhm  32820  zarcmplem  32930  metideq  32942  hauseqcn  32947  tpr2rico  32961  esumrnmpt2  33135  esumpfinvallem  33141  esum2d  33160  omssubadd  33368  carsggect  33386  omsmeas  33391  orvcelval  33536  signsply0  33631  cvmlift2lem11  34373  cvmlift2lem12  34374  dfon2lem7  34830  filnetlem3  35351  onsucsuccmpi  35414  dissneqlem  36307  icoreunrn  36326  ctbssinf  36373  pibt2  36384  mblfinlem1  36611  ismblfin  36615  sstotbnd2  36728  dochexmidlem4  40420  lcfrlem38  40537  mhpind  41248  ismrcd1  41518  eldioph2lem2  41581  rmxyelqirrOLD  41731  hbt  41954  rngunsnply  41997  iocinico  42043  dmtrcl  42460  rntrcl  42461  trrelsuperrel2dg  42504  restuni5  43894  unirnmapsn  43992  limciccioolb  44416  limcrecl  44424  limcicciooub  44432  stoweidlem50  44845  stoweidlem52  44847  stoweidlem53  44848  stoweidlem57  44852  stoweidlem59  44854  fourierdlem50  44951  fourierdlem103  45004  fourierdlem104  45005  pwsal  45110  sge0iun  45214  sge0isum  45222  meadjuni  45252  omessle  45293  rhmimasubrnglem  46823  zlmodzxzel  47110  lincresunit3  47240  amgmwlem  47927