Theorem sseqtrdi 3963

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

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

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  sseqtrrdi  3964  3sstr3g  3975  sofld  6145  relrelss  6231  foimacnv  6791  onfununi  8274  hartogslem1  9450  cantnfp1lem3  9592  uniwf  9734  rankeq0b  9775  djuinf  10102  cflecard  10166  fin23lem16  10248  fin23lem41  10265  pwcfsdom  10497  fpwwe2lem12  10556  fpwwe2  10557  canth4  10561  hashbclem  14405  dmtrclfv  14971  zsum  15671  fsumcvg3  15682  incexclem  15792  zprod  15893  ramub1lem1  16988  setsstruct2  17135  imasaddfnlem  17483  imasvscafn  17492  mremre  17557  submre  17558  mreexexlem3d  17603  isacs1i  17614  acsmapd  18511  acsmap2d  18512  ghmqusnsglem1  19246  gsumzoppg  19910  rhmimasubrnglem  20533  subdrgint  20771  primefld  20773  lspsntri  21084  lsppratlem4  21140  lbsextlem3  21150  sraring  21173  evls1maplmhm  22352  distop  22970  elcls  23048  cnpresti  23263  cnprest  23264  cmpcld  23377  cnconn  23397  iunconn  23403  comppfsc  23507  ptuni2  23551  alexsubALTlem3  24024  ustssco  24190  ust0  24195  ustbas2  24200  ustimasn  24203  utopbas  24210  utop2nei  24225  setsmstopn  24453  metustsym  24530  metust  24533  tngtopn  24625  ovoliunlem1  25479  lhop1lem  25990  ig1peu  26150  ig1pdvds  26155  logccv  26640  amgmlem  26967  upgr1e  29196  uspgr1e  29327  shsupcl  31424  shsupunss  31432  shslubi  31471  orthin  31532  h1datomi  31667  mdslj2i  32406  mdslmd1lem1  32411  iundifdifd  32646  iunxpssiun1  32653  difres  32685  fresf1o  32719  suppovss  32769  swrdrndisj  33032  elrgspnlem3  33320  fracf1  33383  idomsubr  33385  nsgmgclem  33486  ressply1evls1  33640  sradrng  33741  sraidom  33742  resssra  33746  lsssra  33747  extdgfialglem1  33852  extdgfialglem2  33853  zarcmplem  34041  metideq  34053  hauseqcn  34058  tpr2rico  34072  esumrnmpt2  34228  esumpfinvallem  34234  esum2d  34253  omssubadd  34460  carsggect  34478  omsmeas  34483  orvcelval  34629  signsply0  34711  cvmlift2lem11  35511  cvmlift2lem12  35512  dfon2lem7  35985  filnetlem3  36578  onsucsuccmpi  36641  dissneqlem  37670  icoreunrn  37689  ctbssinf  37736  pibt2  37747  mblfinlem1  37992  ismblfin  37996  sstotbnd2  38109  dochexmidlem4  41923  lcfrlem38  42040  rhmqusspan  42638  mhpind  43041  ismrcd1  43144  eldioph2lem2  43207  hbt  43576  rngunsnply  43615  iocinico  43658  dmtrcl  44072  rntrcl  44073  trrelsuperrel2dg  44116  restuni5  45571  unirnmapsn  45661  limciccioolb  46069  limcrecl  46077  limcicciooub  46083  stoweidlem50  46496  stoweidlem52  46498  stoweidlem53  46499  stoweidlem57  46503  stoweidlem59  46505  fourierdlem50  46602  fourierdlem103  46655  fourierdlem104  46656  pwsal  46761  sge0iun  46865  sge0isum  46873  meadjuni  46903  omessle  46944  uhgrimprop  48380  zlmodzxzel  48843  lincresunit3  48969  amgmwlem  50289