Theorem sseqtrdi 3957

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-ss 3902

This theorem is referenced by:  sseqtrrdi  3958  3sstr3g  3969  sofld  6140  relrelss  6226  foimacnv  6786  onfununi  8270  hartogslem1  9446  cantnfp1lem3  9590  uniwf  9732  rankeq0b  9773  djuinf  10100  cflecard  10164  fin23lem16  10246  fin23lem41  10263  pwcfsdom  10495  fpwwe2lem12  10554  fpwwe2  10555  canth4  10559  hashbclem  14403  dmtrclfv  14969  zsum  15669  fsumcvg3  15680  incexclem  15790  zprod  15891  ramub1lem1  16986  setsstruct2  17133  imasaddfnlem  17481  imasvscafn  17490  mremre  17555  submre  17556  mreexexlem3d  17601  isacs1i  17612  acsmapd  18509  acsmap2d  18510  ghmqusnsglem1  19244  gsumzoppg  19908  rhmimasubrnglem  20531  subdrgint  20769  primefld  20771  lspsntri  21081  lsppratlem4  21137  lbsextlem3  21147  sraring  21170  evls1maplmhm  22330  distop  22948  elcls  23026  cnpresti  23241  cnprest  23242  cmpcld  23355  cnconn  23375  iunconn  23381  comppfsc  23485  ptuni2  23529  alexsubALTlem3  24002  ustssco  24168  ust0  24173  ustbas2  24178  ustimasn  24181  utopbas  24188  utop2nei  24203  setsmstopn  24431  metustsym  24508  metust  24511  tngtopn  24603  ovoliunlem1  25457  lhop1lem  25968  ig1peu  26128  ig1pdvds  26133  logccv  26615  amgmlem  26941  upgr1e  29170  uspgr1e  29301  shsupcl  31397  shsupunss  31405  shslubi  31444  orthin  31505  h1datomi  31640  mdslj2i  32379  mdslmd1lem1  32384  iundifdifd  32619  iunxpssiun1  32626  difres  32658  fresf1o  32692  suppovss  32742  swrdrndisj  33005  elrgspnlem3  33293  fracf1  33356  idomsubr  33358  nsgmgclem  33459  ressply1evls1  33613  sradrng  33714  sraidom  33715  resssra  33719  lsssra  33720  extdgfialglem1  33824  extdgfialglem2  33825  zarcmplem  34013  metideq  34025  hauseqcn  34030  tpr2rico  34044  esumrnmpt2  34200  esumpfinvallem  34206  esum2d  34225  omssubadd  34432  carsggect  34450  omsmeas  34455  orvcelval  34601  signsply0  34683  cvmlift2lem11  35483  cvmlift2lem12  35484  dfon2lem7  35957  filnetlem3  36550  onsucsuccmpi  36613  dissneqlem  37644  icoreunrn  37663  ctbssinf  37710  pibt2  37721  mblfinlem1  37966  ismblfin  37970  sstotbnd2  38083  dochexmidlem4  41897  lcfrlem38  42014  rhmqusspan  42612  mhpind  43015  ismrcd1  43118  eldioph2lem2  43181  hbt  43546  rngunsnply  43585  iocinico  43628  dmtrcl  44042  rntrcl  44043  trrelsuperrel2dg  44086  restuni5  45541  unirnmapsn  45631  limciccioolb  46039  limcrecl  46047  limcicciooub  46053  stoweidlem50  46466  stoweidlem52  46468  stoweidlem53  46469  stoweidlem57  46473  stoweidlem59  46475  fourierdlem50  46572  fourierdlem103  46625  fourierdlem104  46626  pwsal  46731  sge0iun  46835  sge0isum  46843  meadjuni  46873  omessle  46914  uhgrimprop  48356  zlmodzxzel  48819  lincresunit3  48945  amgmwlem  50265