Theorem sseqtrdi 3980

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925

This theorem is used by:  sseqtrrdi  3981  3sstr3g  3992  sofld  6190  relrelss  6280  foimacnv  6845  onfununi  8337  hartogslem1  9514  cantnfp1lem3  9659  uniwf  9801  rankeq0b  9842  djuinf  10191  cflecard  10254  fin23lem16  10337  fin23lem41  10354  pwcfsdom  10586  fpwwe2lem12  10645  fpwwe2  10646  canth4  10650  hashbclem  14509  dmtrclfv  15081  zsum  15795  fsumcvg3  15806  incexclem  15916  zprod  16017  ramub1lem1  17111  setsstruct2  17259  imasaddfnlem  17607  imasvscafn  17616  mremre  17681  submre  17682  mreexexlem3d  17727  isacs1i  17738  acsmapd  18635  acsmap2d  18636  ghmqusnsglem1  19381  gsumzoppg  20045  rhmimasubrnglem  20701  subdrgint  20943  primefld  20945  lspsntri  21255  lsppratlem4  21311  lbsextlem3  21321  sraring  21344  evls1maplmhm  22574  distop  23189  elcls  23267  cnpresti  23482  cnprest  23483  cmpcld  23596  cnconn  23616  iunconn  23622  comppfsc  23726  ptuni2  23770  alexsubALTlem3  24243  ustssco  24409  ust0  24414  ustbas2  24419  ustimasn  24422  utopbas  24429  utop2nei  24444  setsmstopn  24672  metustsym  24749  metust  24752  tngtopn  24844  ovoliunlem1  25698  lhop1lem  26209  ig1peu  26369  ig1pdvds  26374  logccv  26865  amgmlem  27191  upgr1e  29500  uspgr1e  29631  shsupcl  31727  shsupunss  31735  shslubi  31774  orthin  31835  h1datomi  31970  mdslj2i  32709  mdslmd1lem1  32714  iundifdifd  32943  iunxpssiun1  32950  difres  32982  fresf1o  33013  suppovss  33063  swrdrndisj  33308  elrgspnlem3  33595  fracf1  33659  idomsubr  33661  nsgmgclem  33751  ressply1evls1  33886  sradrng  34003  sraidom  34004  resssra  34008  lsssra  34009  extdgfialglem1  34113  extdgfialglem2  34114  zarcmplem  34302  metideq  34314  hauseqcn  34319  tpr2rico  34333  esumrnmpt2  34489  esumpfinvallem  34495  esum2d  34514  omssubadd  34722  carsggect  34740  omsmeas  34745  orvcelval  34891  signsply0  34970  cvmlift2lem11  35826  cvmlift2lem12  35827  dfon2lem7  36300  filnetlem3  36932  onsucsuccmpi  36995  dissneqlem  38027  icoreunrn  38046  ctbssinf  38093  pibt2  38104  mblfinlem1  38349  ismblfin  38353  sstotbnd2  38466  dochexmidlem4  42278  lcfrlem38  42395  rhmqusspan  42993  mhpind  43367  ismrcd1  43470  eldioph2lem2  43533  hbt  43898  rngunsnply  43937  iocinico  43980  dmtrcl  44394  rntrcl  44395  trrelsuperrel2dg  44438  restuni5  45882  unirnmapsn  45971  limciccioolb  46378  limcrecl  46386  limcicciooub  46392  stoweidlem50  46805  stoweidlem52  46807  stoweidlem53  46808  stoweidlem57  46812  stoweidlem59  46814  fourierdlem50  46911  fourierdlem103  46964  fourierdlem104  46965  pwsal  47070  sge0iun  47174  sge0isum  47182  meadjuni  47212  omessle  47253  uhgrimprop  48698  zlmodzxzel  49176  lincresunit3  49302  amgmwlem  50691