Theorem sseqtrdi 4033

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sseqtrrdi  4034  sofld  6187  relrelss  6273  foimacnv  6851  onfununi  8341  hartogslem1  9537  cantnfp1lem3  9675  uniwf  9814  rankeq0b  9855  djuinf  10183  cflecard  10248  fin23lem16  10330  fin23lem41  10347  pwcfsdom  10578  fpwwe2lem12  10637  fpwwe2  10638  canth4  10642  hashbclem  14411  dmtrclfv  14965  zsum  15664  fsumcvg3  15675  incexclem  15782  zprod  15881  ramub1lem1  16959  setsstruct2  17107  imasaddfnlem  17474  imasvscafn  17483  mremre  17548  submre  17549  mreexexlem3d  17590  isacs1i  17601  acsmapd  18507  acsmap2d  18508  gsumzoppg  19812  subdrgint  20419  primefld  20421  lspsntri  20708  lsppratlem4  20763  lbsextlem3  20773  sraring  20808  distop  22498  elcls  22577  cnpresti  22792  cnprest  22793  cmpcld  22906  cnconn  22926  iunconn  22932  comppfsc  23036  ptuni2  23080  alexsubALTlem3  23553  ustssco  23719  ust0  23724  ustbas2  23730  ustimasn  23733  utopbas  23740  utop2nei  23755  setsmstopn  23986  metustsym  24064  metust  24067  tngtopn  24167  ovoliunlem1  25019  lhop1lem  25530  ig1peu  25689  ig1pdvds  25694  logccv  26171  amgmlem  26494  upgr1e  28373  uspgr1e  28501  shsupcl  30591  shsupunss  30599  shslubi  30638  orthin  30699  h1datomi  30834  mdslj2i  31573  mdslmd1lem1  31578  iundifdifd  31793  difres  31831  fresf1o  31855  suppovss  31906  swrdrndisj  32121  nsgmgclem  32522  sradrng  32673  evls1maplmhm  32760  zarcmplem  32861  metideq  32873  hauseqcn  32878  tpr2rico  32892  esumrnmpt2  33066  esumpfinvallem  33072  esum2d  33091  omssubadd  33299  carsggect  33317  omsmeas  33322  orvcelval  33467  signsply0  33562  cvmlift2lem11  34304  cvmlift2lem12  34305  dfon2lem7  34761  filnetlem3  35265  onsucsuccmpi  35328  dissneqlem  36221  icoreunrn  36240  ctbssinf  36287  pibt2  36298  mblfinlem1  36525  ismblfin  36529  sstotbnd2  36642  dochexmidlem4  40334  lcfrlem38  40451  mhpind  41166  ismrcd1  41436  eldioph2lem2  41499  rmxyelqirrOLD  41649  hbt  41872  rngunsnply  41915  iocinico  41961  dmtrcl  42378  rntrcl  42379  trrelsuperrel2dg  42422  restuni5  43812  unirnmapsn  43913  limciccioolb  44337  limcrecl  44345  limcicciooub  44353  stoweidlem50  44766  stoweidlem52  44768  stoweidlem53  44769  stoweidlem57  44773  stoweidlem59  44775  fourierdlem50  44872  fourierdlem103  44925  fourierdlem104  44926  pwsal  45031  sge0iun  45135  sge0isum  45143  meadjuni  45173  omessle  45214  rhmimasubrnglem  46744  zlmodzxzel  47031  lincresunit3  47162  amgmwlem  47849