Theorem sseqtrdi 3975

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  sseqtrrdi  3976  3sstr3g  3987  sofld  6134  relrelss  6220  foimacnv  6780  onfununi  8261  hartogslem1  9428  cantnfp1lem3  9570  uniwf  9709  rankeq0b  9750  djuinf  10077  cflecard  10141  fin23lem16  10223  fin23lem41  10240  pwcfsdom  10471  fpwwe2lem12  10530  fpwwe2  10531  canth4  10535  hashbclem  14356  dmtrclfv  14922  zsum  15622  fsumcvg3  15633  incexclem  15740  zprod  15841  ramub1lem1  16935  setsstruct2  17082  imasaddfnlem  17429  imasvscafn  17438  mremre  17503  submre  17504  mreexexlem3d  17549  isacs1i  17560  acsmapd  18457  acsmap2d  18458  ghmqusnsglem1  19190  gsumzoppg  19854  rhmimasubrnglem  20478  subdrgint  20716  primefld  20718  lspsntri  21029  lsppratlem4  21085  lbsextlem3  21095  sraring  21118  evls1maplmhm  22290  distop  22908  elcls  22986  cnpresti  23201  cnprest  23202  cmpcld  23315  cnconn  23335  iunconn  23341  comppfsc  23445  ptuni2  23489  alexsubALTlem3  23962  ustssco  24128  ust0  24133  ustbas2  24138  ustimasn  24141  utopbas  24148  utop2nei  24163  setsmstopn  24391  metustsym  24468  metust  24471  tngtopn  24563  ovoliunlem1  25428  lhop1lem  25943  ig1peu  26105  ig1pdvds  26110  logccv  26597  amgmlem  26925  upgr1e  29089  uspgr1e  29220  shsupcl  31313  shsupunss  31321  shslubi  31360  orthin  31421  h1datomi  31556  mdslj2i  32295  mdslmd1lem1  32300  iundifdifd  32536  iunxpssiun1  32543  difres  32575  fresf1o  32608  suppovss  32657  swrdrndisj  32933  elrgspnlem3  33206  fracf1  33268  idomsubr  33270  nsgmgclem  33371  ressply1evls1  33523  sradrng  33589  sraidom  33590  resssra  33594  lsssra  33595  extdgfialglem1  33700  extdgfialglem2  33701  zarcmplem  33889  metideq  33901  hauseqcn  33906  tpr2rico  33920  esumrnmpt2  34076  esumpfinvallem  34082  esum2d  34101  omssubadd  34308  carsggect  34326  omsmeas  34331  orvcelval  34477  signsply0  34559  cvmlift2lem11  35345  cvmlift2lem12  35346  dfon2lem7  35822  filnetlem3  36413  onsucsuccmpi  36476  dissneqlem  37373  icoreunrn  37392  ctbssinf  37439  pibt2  37450  mblfinlem1  37696  ismblfin  37700  sstotbnd2  37813  dochexmidlem4  41501  lcfrlem38  41618  rhmqusspan  42217  mhpind  42626  ismrcd1  42730  eldioph2lem2  42793  hbt  43162  rngunsnply  43201  iocinico  43244  dmtrcl  43659  rntrcl  43660  trrelsuperrel2dg  43703  restuni5  45159  unirnmapsn  45250  limciccioolb  45660  limcrecl  45668  limcicciooub  45674  stoweidlem50  46087  stoweidlem52  46089  stoweidlem53  46090  stoweidlem57  46094  stoweidlem59  46096  fourierdlem50  46193  fourierdlem103  46246  fourierdlem104  46247  pwsal  46352  sge0iun  46456  sge0isum  46464  meadjuni  46494  omessle  46535  uhgrimprop  47922  zlmodzxzel  48385  lincresunit3  48512  amgmwlem  49833