Theorem sseqtrdi 4032

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-in 3956  df-ss 3966

This theorem is referenced by:  sseqtrrdi  4033  sofld  6196  relrelss  6282  foimacnv  6861  onfununi  8370  hartogslem1  9575  cantnfp1lem3  9713  uniwf  9852  rankeq0b  9893  djuinf  10221  cflecard  10286  fin23lem16  10368  fin23lem41  10385  pwcfsdom  10616  fpwwe2lem12  10675  fpwwe2  10676  canth4  10680  hashbclem  14453  dmtrclfv  15007  zsum  15706  fsumcvg3  15717  incexclem  15824  zprod  15923  ramub1lem1  17004  setsstruct2  17152  imasaddfnlem  17519  imasvscafn  17528  mremre  17593  submre  17594  mreexexlem3d  17635  isacs1i  17646  acsmapd  18555  acsmap2d  18556  gsumzoppg  19913  rhmimasubrnglem  20516  subdrgint  20705  primefld  20707  lspsntri  20996  lsppratlem4  21052  lbsextlem3  21062  sraring  21093  evls1maplmhm  22315  distop  22926  elcls  23005  cnpresti  23220  cnprest  23221  cmpcld  23334  cnconn  23354  iunconn  23360  comppfsc  23464  ptuni2  23508  alexsubALTlem3  23981  ustssco  24147  ust0  24152  ustbas2  24158  ustimasn  24161  utopbas  24168  utop2nei  24183  setsmstopn  24414  metustsym  24492  metust  24495  tngtopn  24595  ovoliunlem1  25459  lhop1lem  25974  ig1peu  26137  ig1pdvds  26142  logccv  26625  amgmlem  26950  upgr1e  28954  uspgr1e  29085  shsupcl  31176  shsupunss  31184  shslubi  31223  orthin  31284  h1datomi  31419  mdslj2i  32158  mdslmd1lem1  32163  iundifdifd  32381  difres  32419  fresf1o  32445  suppovss  32494  swrdrndisj  32707  fracf1  33026  idomsubr  33028  nsgmgclem  33154  ghmqusnsglem1  33162  sradrng  33324  resssra  33328  lsssra  33329  zarcmplem  33523  metideq  33535  hauseqcn  33540  tpr2rico  33554  esumrnmpt2  33728  esumpfinvallem  33734  esum2d  33753  omssubadd  33961  carsggect  33979  omsmeas  33984  orvcelval  34129  signsply0  34224  cvmlift2lem11  34964  cvmlift2lem12  34965  dfon2lem7  35426  filnetlem3  35905  onsucsuccmpi  35968  dissneqlem  36860  icoreunrn  36879  ctbssinf  36926  pibt2  36937  mblfinlem1  37171  ismblfin  37175  sstotbnd2  37288  dochexmidlem4  40976  lcfrlem38  41093  mhpind  41876  ismrcd1  42167  eldioph2lem2  42230  rmxyelqirrOLD  42380  hbt  42603  rngunsnply  42646  iocinico  42689  dmtrcl  43106  rntrcl  43107  trrelsuperrel2dg  43150  restuni5  44538  unirnmapsn  44635  limciccioolb  45056  limcrecl  45064  limcicciooub  45072  stoweidlem50  45485  stoweidlem52  45487  stoweidlem53  45488  stoweidlem57  45492  stoweidlem59  45494  fourierdlem50  45591  fourierdlem103  45644  fourierdlem104  45645  pwsal  45750  sge0iun  45854  sge0isum  45862  meadjuni  45892  omessle  45933  zlmodzxzel  47515  lincresunit3  47645  amgmwlem  48331