Theorem sseqtrdi 3976

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

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  sseqtrrdi  3977  3sstr3g  3988  sofld  6169  relrelss  6256  foimacnv  6820  onfununi  8307  hartogslem1  9487  cantnfp1lem3  9632  uniwf  9774  rankeq0b  9815  djuinf  10142  cflecard  10206  fin23lem16  10289  fin23lem41  10306  pwcfsdom  10538  fpwwe2lem12  10597  fpwwe2  10598  canth4  10602  hashbclem  14462  dmtrclfv  15028  zsum  15728  fsumcvg3  15739  incexclem  15849  zprod  15950  ramub1lem1  17045  setsstruct2  17193  imasaddfnlem  17541  imasvscafn  17550  mremre  17615  submre  17616  mreexexlem3d  17661  isacs1i  17672  acsmapd  18569  acsmap2d  18570  ghmqusnsglem1  19303  gsumzoppg  19967  rhmimasubrnglem  20594  subdrgint  20832  primefld  20834  lspsntri  21144  lsppratlem4  21200  lbsextlem3  21210  sraring  21233  evls1maplmhm  22420  distop  23035  elcls  23113  cnpresti  23328  cnprest  23329  cmpcld  23442  cnconn  23462  iunconn  23468  comppfsc  23572  ptuni2  23616  alexsubALTlem3  24089  ustssco  24255  ust0  24260  ustbas2  24265  ustimasn  24268  utopbas  24275  utop2nei  24290  setsmstopn  24518  metustsym  24595  metust  24598  tngtopn  24690  ovoliunlem1  25544  lhop1lem  26055  ig1peu  26215  ig1pdvds  26220  logccv  26705  amgmlem  27031  upgr1e  29260  uspgr1e  29391  shsupcl  31487  shsupunss  31495  shslubi  31534  orthin  31595  h1datomi  31730  mdslj2i  32469  mdslmd1lem1  32474  iundifdifd  32710  iunxpssiun1  32717  difres  32749  fresf1o  32783  suppovss  32833  swrdrndisj  33096  elrgspnlem3  33386  fracf1  33455  idomsubr  33457  nsgmgclem  33558  ressply1evls1  33722  sradrng  33840  sraidom  33841  resssra  33845  lsssra  33846  extdgfialglem1  33950  extdgfialglem2  33951  zarcmplem  34139  metideq  34151  hauseqcn  34156  tpr2rico  34170  esumrnmpt2  34326  esumpfinvallem  34332  esum2d  34351  omssubadd  34558  carsggect  34576  omsmeas  34581  orvcelval  34727  signsply0  34809  cvmlift2lem11  35627  cvmlift2lem12  35628  dfon2lem7  36101  filnetlem3  36704  onsucsuccmpi  36767  dissneqlem  37798  icoreunrn  37817  ctbssinf  37864  pibt2  37875  mblfinlem1  38120  ismblfin  38124  sstotbnd2  38237  dochexmidlem4  42051  lcfrlem38  42168  rhmqusspan  42766  mhpind  43140  ismrcd1  43243  eldioph2lem2  43306  hbt  43671  rngunsnply  43710  iocinico  43753  dmtrcl  44167  rntrcl  44168  trrelsuperrel2dg  44211  restuni5  45665  unirnmapsn  45754  limciccioolb  46161  limcrecl  46169  limcicciooub  46175  stoweidlem50  46588  stoweidlem52  46590  stoweidlem53  46591  stoweidlem57  46595  stoweidlem59  46597  fourierdlem50  46694  fourierdlem103  46747  fourierdlem104  46748  pwsal  46853  sge0iun  46957  sge0isum  46965  meadjuni  46995  omessle  47036  uhgrimprop  48478  zlmodzxzel  48941  lincresunit3  49067  amgmwlem  50387