Theorem sseqtrdi 4004

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ss 3948

This theorem is referenced by:  sseqtrrdi  4005  3sstr3g  4016  sofld  6181  relrelss  6267  foimacnv  6840  onfununi  8360  hartogslem1  9561  cantnfp1lem3  9699  uniwf  9838  rankeq0b  9879  djuinf  10208  cflecard  10272  fin23lem16  10354  fin23lem41  10371  pwcfsdom  10602  fpwwe2lem12  10661  fpwwe2  10662  canth4  10666  hashbclem  14475  dmtrclfv  15042  zsum  15739  fsumcvg3  15750  incexclem  15857  zprod  15958  ramub1lem1  17051  setsstruct2  17198  imasaddfnlem  17547  imasvscafn  17556  mremre  17621  submre  17622  mreexexlem3d  17663  isacs1i  17674  acsmapd  18569  acsmap2d  18570  ghmqusnsglem1  19268  gsumzoppg  19930  rhmimasubrnglem  20530  subdrgint  20768  primefld  20770  lspsntri  21060  lsppratlem4  21116  lbsextlem3  21126  sraring  21149  evls1maplmhm  22320  distop  22938  elcls  23016  cnpresti  23231  cnprest  23232  cmpcld  23345  cnconn  23365  iunconn  23371  comppfsc  23475  ptuni2  23519  alexsubALTlem3  23992  ustssco  24158  ust0  24163  ustbas2  24169  ustimasn  24172  utopbas  24179  utop2nei  24194  setsmstopn  24422  metustsym  24499  metust  24502  tngtopn  24594  ovoliunlem1  25460  lhop1lem  25975  ig1peu  26137  ig1pdvds  26142  logccv  26629  amgmlem  26957  upgr1e  29097  uspgr1e  29228  shsupcl  31324  shsupunss  31332  shslubi  31371  orthin  31432  h1datomi  31567  mdslj2i  32306  mdslmd1lem1  32311  iundifdifd  32547  iunxpssiun1  32554  difres  32586  fresf1o  32614  suppovss  32663  swrdrndisj  32938  elrgspnlem3  33244  fracf1  33306  idomsubr  33308  nsgmgclem  33431  ressply1evls1  33583  sradrng  33627  sraidom  33628  resssra  33632  lsssra  33633  zarcmplem  33917  metideq  33929  hauseqcn  33934  tpr2rico  33948  esumrnmpt2  34104  esumpfinvallem  34110  esum2d  34129  omssubadd  34337  carsggect  34355  omsmeas  34360  orvcelval  34506  signsply0  34588  cvmlift2lem11  35340  cvmlift2lem12  35341  dfon2lem7  35812  filnetlem3  36403  onsucsuccmpi  36466  dissneqlem  37363  icoreunrn  37382  ctbssinf  37429  pibt2  37440  mblfinlem1  37686  ismblfin  37690  sstotbnd2  37803  dochexmidlem4  41487  lcfrlem38  41604  rhmqusspan  42203  mhpind  42584  ismrcd1  42688  eldioph2lem2  42751  rmxyelqirrOLD  42901  hbt  43121  rngunsnply  43160  iocinico  43203  dmtrcl  43618  rntrcl  43619  trrelsuperrel2dg  43662  restuni5  45114  unirnmapsn  45205  limciccioolb  45617  limcrecl  45625  limcicciooub  45633  stoweidlem50  46046  stoweidlem52  46048  stoweidlem53  46049  stoweidlem57  46053  stoweidlem59  46055  fourierdlem50  46152  fourierdlem103  46205  fourierdlem104  46206  pwsal  46311  sge0iun  46415  sge0isum  46423  meadjuni  46453  omessle  46494  uhgrimprop  47872  zlmodzxzel  48297  lincresunit3  48424  amgmwlem  49633