Theorem sseqtrdi 3948

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseqtrrdi  3949  3sstr3g  3960  sofld  6178  relrelss  6275  foimacnv  6843  onfununi  8353  hartogslem1  9540  cantnfp1lem3  9685  uniwf  9832  rankeq0b  9880  djuinf  10271  cflecard  10334  fin23lem16  10417  fin23lem41  10434  pwcfsdom  10672  fpwwe2lem12  10731  fpwwe2  10732  canth4  10736  hashbclem  14601  dmtrclfv  15177  zsum  15890  fsumcvg3  15901  incexclem  16011  zprod  16110  ramub1lem1  17210  setsstruct2  17358  imasaddfnlem  17706  imasvscafn  17715  mremre  17780  submre  17781  mreexexlem3d  17826  isacs1i  17837  acsmapd  18734  acsmap2d  18735  ghmqusnsglem1  19500  gsumzoppg  20164  rhmimasubrnglem  20823  subdrgint  21066  primefld  21068  lspsntri  21378  lsppratlem4  21434  lbsextlem3  21444  sraring  21467  evls1maplmhm  22701  distop  23319  elcls  23397  cnpresti  23612  cnprest  23613  cmpcld  23726  cnconn  23746  iunconn  23752  comppfsc  23857  ptuni2  23901  alexsubALTlem3  24374  ustssco  24540  ust0  24545  ustbas2  24550  ustimasn  24553  utopbas  24560  utop2nei  24575  setsmstopn  24803  metustsym  24880  metust  24883  tngtopn  24975  ovoliunlem1  25829  lhop1lem  26339  ig1peu  26499  ig1pdvds  26504  logccv  26997  amgmlem  27323  upgr1e  29697  uspgr1e  29831  shsupcl  31946  shsupunss  31954  shslubi  31993  orthin  32054  h1datomi  32189  mdslj2i  32928  mdslmd1lem1  32933  iundifdifd  33204  iunxpssiun1  33210  difres  33242  fresf1o  33273  suppovss  33322  swrdrndisj  33565  elrgspnlem3  33852  fracf1  33916  idomsubr  33918  nsgmgclem  34009  ressply1evls1  34144  sradrng  34261  sraidom  34262  resssra  34266  lsssra  34267  extdgfialglem1  34371  extdgfialglem2  34372  zarcmplem  34560  metideq  34572  hauseqcn  34577  tpr2rico  34591  esumrnmpt2  34747  esumpfinvallem  34753  esum2d  34772  omssubadd  34979  carsggect  34997  omsmeas  35002  orvcelval  35148  signsply0  35227  cvmlift2lem11  36165  cvmlift2lem12  36166  dfon2lem7  36644  filnetlem3  37261  onsucsuccmpi  37324  dissneqlem  38357  icoreunrn  38376  ctbssinf  38423  pibt2  38434  mblfinlem1  38669  ismblfin  38673  sstotbnd2  38802  dochexmidlem4  42614  lcfrlem38  42731  rhmqusspan  43329  mhpind  43716  ismrcd1  43803  eldioph2lem2  43866  hbt  44226  rngunsnply  44265  iocinico  44308  dmtrcl  44721  rntrcl  44722  trrelsuperrel2dg  44765  restuni5  46232  unirnmapsn  46321  limciccioolb  46727  limcrecl  46735  limcicciooub  46741  stoweidlem50  47154  stoweidlem52  47156  stoweidlem53  47157  stoweidlem57  47161  stoweidlem59  47163  fourierdlem50  47260  fourierdlem103  47313  fourierdlem104  47314  pwsal  47419  sge0iun  47523  sge0isum  47531  meadjuni  47561  omessle  47602  uhgrimprop  49084  zlmodzxzel  49561  lincresunit3  49687  amgmwlem  51156