Theorem sseqtrdi 3974

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  sseqtrrdi  3975  3sstr3g  3986  sofld  6145  relrelss  6231  foimacnv  6791  onfununi  8273  hartogslem1  9447  cantnfp1lem3  9589  uniwf  9731  rankeq0b  9772  djuinf  10099  cflecard  10163  fin23lem16  10245  fin23lem41  10262  pwcfsdom  10494  fpwwe2lem12  10553  fpwwe2  10554  canth4  10558  hashbclem  14375  dmtrclfv  14941  zsum  15641  fsumcvg3  15652  incexclem  15759  zprod  15860  ramub1lem1  16954  setsstruct2  17101  imasaddfnlem  17449  imasvscafn  17458  mremre  17523  submre  17524  mreexexlem3d  17569  isacs1i  17580  acsmapd  18477  acsmap2d  18478  ghmqusnsglem1  19209  gsumzoppg  19873  rhmimasubrnglem  20498  subdrgint  20736  primefld  20738  lspsntri  21049  lsppratlem4  21105  lbsextlem3  21115  sraring  21138  evls1maplmhm  22321  distop  22939  elcls  23017  cnpresti  23232  cnprest  23233  cmpcld  23346  cnconn  23366  iunconn  23372  comppfsc  23476  ptuni2  23520  alexsubALTlem3  23993  ustssco  24159  ust0  24164  ustbas2  24169  ustimasn  24172  utopbas  24179  utop2nei  24194  setsmstopn  24422  metustsym  24499  metust  24502  tngtopn  24594  ovoliunlem1  25459  lhop1lem  25974  ig1peu  26136  ig1pdvds  26141  logccv  26628  amgmlem  26956  upgr1e  29186  uspgr1e  29317  shsupcl  31413  shsupunss  31421  shslubi  31460  orthin  31521  h1datomi  31656  mdslj2i  32395  mdslmd1lem1  32400  iundifdifd  32636  iunxpssiun1  32643  difres  32675  fresf1o  32709  suppovss  32760  swrdrndisj  33039  elrgspnlem3  33326  fracf1  33389  idomsubr  33391  nsgmgclem  33492  ressply1evls1  33646  sradrng  33738  sraidom  33739  resssra  33743  lsssra  33744  extdgfialglem1  33849  extdgfialglem2  33850  zarcmplem  34038  metideq  34050  hauseqcn  34055  tpr2rico  34069  esumrnmpt2  34225  esumpfinvallem  34231  esum2d  34250  omssubadd  34457  carsggect  34475  omsmeas  34480  orvcelval  34626  signsply0  34708  cvmlift2lem11  35507  cvmlift2lem12  35508  dfon2lem7  35981  filnetlem3  36574  onsucsuccmpi  36637  dissneqlem  37541  icoreunrn  37560  ctbssinf  37607  pibt2  37618  mblfinlem1  37854  ismblfin  37858  sstotbnd2  37971  dochexmidlem4  41719  lcfrlem38  41836  rhmqusspan  42435  mhpind  42833  ismrcd1  42936  eldioph2lem2  42999  hbt  43368  rngunsnply  43407  iocinico  43450  dmtrcl  43864  rntrcl  43865  trrelsuperrel2dg  43908  restuni5  45363  unirnmapsn  45454  limciccioolb  45863  limcrecl  45871  limcicciooub  45877  stoweidlem50  46290  stoweidlem52  46292  stoweidlem53  46293  stoweidlem57  46297  stoweidlem59  46299  fourierdlem50  46396  fourierdlem103  46449  fourierdlem104  46450  pwsal  46555  sge0iun  46659  sge0isum  46667  meadjuni  46697  omessle  46738  uhgrimprop  48134  zlmodzxzel  48597  lincresunit3  48723  amgmwlem  50043