Theorem sseqtrdi 3971

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  sseqtrrdi  3972  3sstr3g  3983  sofld  6178  relrelss  6268  foimacnv  6834  onfununi  8333  hartogslem1  9520  cantnfp1lem3  9665  uniwf  9809  rankeq0b  9857  djuinf  10248  cflecard  10311  fin23lem16  10394  fin23lem41  10411  pwcfsdom  10649  fpwwe2lem12  10708  fpwwe2  10709  canth4  10713  hashbclem  14577  dmtrclfv  15151  zsum  15864  fsumcvg3  15875  incexclem  15985  zprod  16084  ramub1lem1  17184  setsstruct2  17332  imasaddfnlem  17680  imasvscafn  17689  mremre  17754  submre  17755  mreexexlem3d  17800  isacs1i  17811  acsmapd  18708  acsmap2d  18709  ghmqusnsglem1  19474  gsumzoppg  20138  rhmimasubrnglem  20797  subdrgint  21040  primefld  21042  lspsntri  21352  lsppratlem4  21408  lbsextlem3  21418  sraring  21441  evls1maplmhm  22675  distop  23293  elcls  23371  cnpresti  23586  cnprest  23587  cmpcld  23700  cnconn  23720  iunconn  23726  comppfsc  23831  ptuni2  23875  alexsubALTlem3  24348  ustssco  24514  ust0  24519  ustbas2  24524  ustimasn  24527  utopbas  24534  utop2nei  24549  setsmstopn  24777  metustsym  24854  metust  24857  tngtopn  24949  ovoliunlem1  25803  lhop1lem  26313  ig1peu  26473  ig1pdvds  26478  logccv  26973  amgmlem  27299  upgr1e  29673  uspgr1e  29807  shsupcl  31922  shsupunss  31930  shslubi  31969  orthin  32030  h1datomi  32165  mdslj2i  32904  mdslmd1lem1  32909  iundifdifd  33138  iunxpssiun1  33144  difres  33176  fresf1o  33207  suppovss  33256  swrdrndisj  33500  elrgspnlem3  33787  fracf1  33851  idomsubr  33853  nsgmgclem  33944  ressply1evls1  34079  sradrng  34196  sraidom  34197  resssra  34201  lsssra  34202  extdgfialglem1  34306  extdgfialglem2  34307  zarcmplem  34495  metideq  34507  hauseqcn  34512  tpr2rico  34526  esumrnmpt2  34682  esumpfinvallem  34688  esum2d  34707  omssubadd  34915  carsggect  34933  omsmeas  34938  orvcelval  35084  signsply0  35163  cvmlift2lem11  36047  cvmlift2lem12  36048  dfon2lem7  36521  filnetlem3  37138  onsucsuccmpi  37201  dissneqlem  38231  icoreunrn  38250  ctbssinf  38297  pibt2  38308  mblfinlem1  38543  ismblfin  38547  sstotbnd2  38676  dochexmidlem4  42488  lcfrlem38  42605  rhmqusspan  43203  mhpind  43584  ismrcd1  43662  eldioph2lem2  43725  hbt  44090  rngunsnply  44129  iocinico  44172  dmtrcl  44586  rntrcl  44587  trrelsuperrel2dg  44630  restuni5  46081  unirnmapsn  46170  limciccioolb  46577  limcrecl  46585  limcicciooub  46591  stoweidlem50  47004  stoweidlem52  47006  stoweidlem53  47007  stoweidlem57  47011  stoweidlem59  47013  fourierdlem50  47110  fourierdlem103  47163  fourierdlem104  47164  pwsal  47269  sge0iun  47373  sge0isum  47381  meadjuni  47411  omessle  47452  uhgrimprop  48934  zlmodzxzel  49411  lincresunit3  49537  amgmwlem  50931