Theorem sseqtrdi 3965

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  sseqtrrdi  3966  sofld  6011  relrelss  6092  foimacnv  6607  onfununi  7961  hartogslem1  8990  cantnfp1lem3  9127  uniwf  9232  rankeq0b  9273  djuinf  9599  cflecard  9664  fin23lem16  9746  fin23lem41  9763  pwcfsdom  9994  fpwwe2lem13  10053  fpwwe2  10054  canth4  10058  hashbclem  13806  dmtrclfv  14369  zsum  15067  fsumcvg3  15078  incexclem  15183  zprod  15283  ramub1lem1  16352  setsstruct2  16513  imasaddfnlem  16793  imasvscafn  16802  mremre  16867  submre  16868  mreexexlem3d  16909  isacs1i  16920  acsmapd  17780  acsmap2d  17781  gsumzoppg  19057  subdrgint  19575  primefld  19577  lspsntri  19862  lsppratlem4  19915  lbsextlem3  19925  distop  21600  elcls  21678  cnpresti  21893  cnprest  21894  cmpcld  22007  cnconn  22027  iunconn  22033  comppfsc  22137  ptuni2  22181  alexsubALTlem3  22654  ustssco  22820  ust0  22825  ustbas2  22831  ustimasn  22834  utopbas  22841  utop2nei  22856  setsmstopn  23085  metustsym  23162  metust  23165  tngtopn  23256  ovoliunlem1  24106  lhop1lem  24616  ig1peu  24772  ig1pdvds  24777  logccv  25254  amgmlem  25575  upgr1e  26906  uspgr1e  27034  shsupcl  29121  shsupunss  29129  shslubi  29168  orthin  29229  h1datomi  29364  mdslj2i  30103  mdslmd1lem1  30108  iundifdifd  30325  difres  30363  fresf1o  30390  suppovss  30443  swrdrndisj  30657  sraring  31075  sradrng  31076  zarcmplem  31234  metideq  31246  hauseqcn  31251  tpr2rico  31265  esumrnmpt2  31437  esumpfinvallem  31443  esum2d  31462  omssubadd  31668  carsggect  31686  omsmeas  31691  orvcelval  31836  signsply0  31931  cvmlift2lem11  32673  cvmlift2lem12  32674  dfon2lem7  33147  filnetlem3  33841  onsucsuccmpi  33904  dissneqlem  34757  icoreunrn  34776  ctbssinf  34823  pibt2  34834  mblfinlem1  35094  ismblfin  35098  sstotbnd2  35212  dochexmidlem4  38759  lcfrlem38  38876  ismrcd1  39639  eldioph2lem2  39702  rmxyelqirr  39851  hbt  40074  rngunsnply  40117  iocinico  40162  dmtrcl  40327  rntrcl  40328  trrelsuperrel2dg  40372  restuni5  41758  unirnmapsn  41843  limciccioolb  42263  limcrecl  42271  limcicciooub  42279  stoweidlem50  42692  stoweidlem52  42694  stoweidlem53  42695  stoweidlem57  42699  stoweidlem59  42701  fourierdlem50  42798  fourierdlem103  42851  fourierdlem104  42852  pwsal  42957  sge0iun  43058  sge0isum  43066  meadjuni  43096  omessle  43137  zlmodzxzel  44757  lincresunit3  44890  amgmwlem  45330