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 221	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 2155  ax-ext 2734

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

This theorem is used by:  sseqtrrdi  3975  3sstr3g  3986  sofld  6184  relrelss  6274  foimacnv  6839  onfununi  8334  hartogslem1  9518  cantnfp1lem3  9663  uniwf  9805  rankeq0b  9846  djuinf  10195  cflecard  10258  fin23lem16  10341  fin23lem41  10358  pwcfsdom  10596  fpwwe2lem12  10655  fpwwe2  10656  canth4  10660  hashbclem  14521  dmtrclfv  15095  zsum  15808  fsumcvg3  15819  incexclem  15929  zprod  16030  ramub1lem1  17124  setsstruct2  17272  imasaddfnlem  17620  imasvscafn  17629  mremre  17694  submre  17695  mreexexlem3d  17740  isacs1i  17751  acsmapd  18648  acsmap2d  18649  ghmqusnsglem1  19413  gsumzoppg  20077  rhmimasubrnglem  20733  subdrgint  20975  primefld  20977  lspsntri  21287  lsppratlem4  21343  lbsextlem3  21353  sraring  21376  evls1maplmhm  22608  distop  23226  elcls  23304  cnpresti  23519  cnprest  23520  cmpcld  23633  cnconn  23653  iunconn  23659  comppfsc  23764  ptuni2  23808  alexsubALTlem3  24281  ustssco  24447  ust0  24452  ustbas2  24457  ustimasn  24460  utopbas  24467  utop2nei  24482  setsmstopn  24710  metustsym  24787  metust  24790  tngtopn  24882  ovoliunlem1  25736  lhop1lem  26247  ig1peu  26407  ig1pdvds  26412  logccv  26908  amgmlem  27234  upgr1e  29578  uspgr1e  29712  shsupcl  31827  shsupunss  31835  shslubi  31874  orthin  31935  h1datomi  32070  mdslj2i  32809  mdslmd1lem1  32814  iundifdifd  33043  iunxpssiun1  33049  difres  33081  fresf1o  33112  suppovss  33161  swrdrndisj  33405  elrgspnlem3  33692  fracf1  33756  idomsubr  33758  nsgmgclem  33848  ressply1evls1  33983  sradrng  34100  sraidom  34101  resssra  34105  lsssra  34106  extdgfialglem1  34210  extdgfialglem2  34211  zarcmplem  34399  metideq  34411  hauseqcn  34416  tpr2rico  34430  esumrnmpt2  34586  esumpfinvallem  34592  esum2d  34611  omssubadd  34819  carsggect  34837  omsmeas  34842  orvcelval  34988  signsply0  35067  cvmlift2lem11  35900  cvmlift2lem12  35901  dfon2lem7  36374  filnetlem3  37007  onsucsuccmpi  37070  dissneqlem  38102  icoreunrn  38121  ctbssinf  38168  pibt2  38179  mblfinlem1  38414  ismblfin  38418  sstotbnd2  38532  dochexmidlem4  42344  lcfrlem38  42461  rhmqusspan  43059  mhpind  43448  ismrcd1  43551  eldioph2lem2  43614  hbt  43979  rngunsnply  44018  iocinico  44061  dmtrcl  44475  rntrcl  44476  trrelsuperrel2dg  44519  restuni5  45963  unirnmapsn  46052  limciccioolb  46459  limcrecl  46467  limcicciooub  46473  stoweidlem50  46886  stoweidlem52  46888  stoweidlem53  46889  stoweidlem57  46893  stoweidlem59  46895  fourierdlem50  46992  fourierdlem103  47045  fourierdlem104  47046  pwsal  47151  sge0iun  47255  sge0isum  47263  meadjuni  47293  omessle  47334  uhgrimprop  48816  zlmodzxzel  49293  lincresunit3  49419  amgmwlem  50828