Theorem sseqtrdi 3979

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

Syntax hints:   → wi 4   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  sseqtrrdi  3980  3sstr3g  3991  sofld  6177  relrelss  6264  foimacnv  6828  onfununi  8316  hartogslem1  9492  cantnfp1lem3  9637  uniwf  9779  rankeq0b  9820  djuinf  10160  cflecard  10224  fin23lem16  10307  fin23lem41  10324  pwcfsdom  10556  fpwwe2lem12  10615  fpwwe2  10616  canth4  10620  hashbclem  14479  dmtrclfv  15045  zsum  15759  fsumcvg3  15770  incexclem  15880  zprod  15981  ramub1lem1  17076  setsstruct2  17224  imasaddfnlem  17572  imasvscafn  17581  mremre  17646  submre  17647  mreexexlem3d  17692  isacs1i  17703  acsmapd  18600  acsmap2d  18601  ghmqusnsglem1  19341  gsumzoppg  20005  rhmimasubrnglem  20641  subdrgint  20875  primefld  20877  lspsntri  21187  lsppratlem4  21243  lbsextlem3  21253  sraring  21276  evls1maplmhm  22498  distop  23113  elcls  23191  cnpresti  23406  cnprest  23407  cmpcld  23520  cnconn  23540  iunconn  23546  comppfsc  23650  ptuni2  23694  alexsubALTlem3  24167  ustssco  24333  ust0  24338  ustbas2  24343  ustimasn  24346  utopbas  24353  utop2nei  24368  setsmstopn  24596  metustsym  24673  metust  24676  tngtopn  24768  ovoliunlem1  25622  lhop1lem  26133  ig1peu  26293  ig1pdvds  26298  logccv  26786  amgmlem  27112  upgr1e  29372  uspgr1e  29503  shsupcl  31599  shsupunss  31607  shslubi  31646  orthin  31707  h1datomi  31842  mdslj2i  32581  mdslmd1lem1  32586  iundifdifd  32816  iunxpssiun1  32823  difres  32855  fresf1o  32888  suppovss  32938  swrdrndisj  33190  elrgspnlem3  33477  fracf1  33543  idomsubr  33545  nsgmgclem  33636  ressply1evls1  33772  sradrng  33889  sraidom  33890  resssra  33894  lsssra  33895  extdgfialglem1  33999  extdgfialglem2  34000  zarcmplem  34188  metideq  34200  hauseqcn  34205  tpr2rico  34219  esumrnmpt2  34375  esumpfinvallem  34381  esum2d  34400  omssubadd  34607  carsggect  34625  omsmeas  34630  orvcelval  34776  signsply0  34855  cvmlift2lem11  35676  cvmlift2lem12  35677  dfon2lem7  36150  filnetlem3  36753  onsucsuccmpi  36816  dissneqlem  37846  icoreunrn  37865  ctbssinf  37912  pibt2  37923  mblfinlem1  38168  ismblfin  38172  sstotbnd2  38285  dochexmidlem4  42099  lcfrlem38  42216  rhmqusspan  42814  mhpind  43188  ismrcd1  43291  eldioph2lem2  43354  hbt  43719  rngunsnply  43758  iocinico  43801  dmtrcl  44215  rntrcl  44216  trrelsuperrel2dg  44259  restuni5  45699  unirnmapsn  45788  limciccioolb  46195  limcrecl  46203  limcicciooub  46209  stoweidlem50  46622  stoweidlem52  46624  stoweidlem53  46625  stoweidlem57  46629  stoweidlem59  46631  fourierdlem50  46728  fourierdlem103  46781  fourierdlem104  46782  pwsal  46887  sge0iun  46991  sge0isum  46999  meadjuni  47029  omessle  47070  uhgrimprop  48512  zlmodzxzel  48986  lincresunit3  49112  amgmwlem  50431