Theorem sseqtrdi 3962

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  sseqtrrdi  3963  3sstr3g  3974  sofld  6145  relrelss  6231  foimacnv  6791  onfununi  8278  hartogslem1  9454  cantnfp1lem3  9599  uniwf  9741  rankeq0b  9782  djuinf  10109  cflecard  10173  fin23lem16  10255  fin23lem41  10272  pwcfsdom  10504  fpwwe2lem12  10563  fpwwe2  10564  canth4  10568  hashbclem  14412  dmtrclfv  14978  zsum  15678  fsumcvg3  15689  incexclem  15799  zprod  15900  ramub1lem1  16995  setsstruct2  17142  imasaddfnlem  17490  imasvscafn  17499  mremre  17564  submre  17565  mreexexlem3d  17610  isacs1i  17621  acsmapd  18518  acsmap2d  18519  ghmqusnsglem1  19253  gsumzoppg  19917  rhmimasubrnglem  20544  subdrgint  20782  primefld  20784  lspsntri  21094  lsppratlem4  21150  lbsextlem3  21160  sraring  21183  evls1maplmhm  22370  distop  22985  elcls  23063  cnpresti  23278  cnprest  23279  cmpcld  23392  cnconn  23412  iunconn  23418  comppfsc  23522  ptuni2  23566  alexsubALTlem3  24039  ustssco  24205  ust0  24210  ustbas2  24215  ustimasn  24218  utopbas  24225  utop2nei  24240  setsmstopn  24468  metustsym  24545  metust  24548  tngtopn  24640  ovoliunlem1  25494  lhop1lem  26005  ig1peu  26165  ig1pdvds  26170  logccv  26652  amgmlem  26978  upgr1e  29207  uspgr1e  29338  shsupcl  31434  shsupunss  31442  shslubi  31481  orthin  31542  h1datomi  31677  mdslj2i  32416  mdslmd1lem1  32421  iundifdifd  32657  iunxpssiun1  32664  difres  32696  fresf1o  32730  suppovss  32780  swrdrndisj  33043  elrgspnlem3  33332  fracf1  33398  idomsubr  33400  nsgmgclem  33501  ressply1evls1  33655  sradrng  33773  sraidom  33774  resssra  33778  lsssra  33779  extdgfialglem1  33883  extdgfialglem2  33884  zarcmplem  34072  metideq  34084  hauseqcn  34089  tpr2rico  34103  esumrnmpt2  34259  esumpfinvallem  34265  esum2d  34284  omssubadd  34491  carsggect  34509  omsmeas  34514  orvcelval  34660  signsply0  34742  cvmlift2lem11  35548  cvmlift2lem12  35549  dfon2lem7  36022  filnetlem3  36615  onsucsuccmpi  36678  dissneqlem  37709  icoreunrn  37728  ctbssinf  37775  pibt2  37786  mblfinlem1  38031  ismblfin  38035  sstotbnd2  38148  dochexmidlem4  41962  lcfrlem38  42079  rhmqusspan  42677  mhpind  43051  ismrcd1  43154  eldioph2lem2  43217  hbt  43582  rngunsnply  43621  iocinico  43664  dmtrcl  44078  rntrcl  44079  trrelsuperrel2dg  44122  restuni5  45577  unirnmapsn  45666  limciccioolb  46073  limcrecl  46081  limcicciooub  46087  stoweidlem50  46500  stoweidlem52  46502  stoweidlem53  46503  stoweidlem57  46507  stoweidlem59  46509  fourierdlem50  46606  fourierdlem103  46659  fourierdlem104  46660  pwsal  46765  sge0iun  46869  sge0isum  46877  meadjuni  46907  omessle  46948  uhgrimprop  48390  zlmodzxzel  48853  lincresunit3  48979  amgmwlem  50299