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 1541   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  sseqtrrdi  4033  sofld  6186  relrelss  6272  foimacnv  6850  onfununi  8340  hartogslem1  9536  cantnfp1lem3  9674  uniwf  9813  rankeq0b  9854  djuinf  10182  cflecard  10247  fin23lem16  10329  fin23lem41  10346  pwcfsdom  10577  fpwwe2lem12  10636  fpwwe2  10637  canth4  10641  hashbclem  14410  dmtrclfv  14964  zsum  15663  fsumcvg3  15674  incexclem  15781  zprod  15880  ramub1lem1  16958  setsstruct2  17106  imasaddfnlem  17473  imasvscafn  17482  mremre  17547  submre  17548  mreexexlem3d  17589  isacs1i  17600  acsmapd  18506  acsmap2d  18507  gsumzoppg  19811  subdrgint  20418  primefld  20420  lspsntri  20707  lsppratlem4  20762  lbsextlem3  20772  sraring  20807  distop  22497  elcls  22576  cnpresti  22791  cnprest  22792  cmpcld  22905  cnconn  22925  iunconn  22931  comppfsc  23035  ptuni2  23079  alexsubALTlem3  23552  ustssco  23718  ust0  23723  ustbas2  23729  ustimasn  23732  utopbas  23739  utop2nei  23754  setsmstopn  23985  metustsym  24063  metust  24066  tngtopn  24166  ovoliunlem1  25018  lhop1lem  25529  ig1peu  25688  ig1pdvds  25693  logccv  26170  amgmlem  26491  upgr1e  28370  uspgr1e  28498  shsupcl  30586  shsupunss  30594  shslubi  30633  orthin  30694  h1datomi  30829  mdslj2i  31568  mdslmd1lem1  31573  iundifdifd  31788  difres  31826  fresf1o  31850  suppovss  31901  swrdrndisj  32116  nsgmgclem  32517  sradrng  32668  evls1maplmhm  32755  zarcmplem  32856  metideq  32868  hauseqcn  32873  tpr2rico  32887  esumrnmpt2  33061  esumpfinvallem  33067  esum2d  33086  omssubadd  33294  carsggect  33312  omsmeas  33317  orvcelval  33462  signsply0  33557  cvmlift2lem11  34299  cvmlift2lem12  34300  dfon2lem7  34756  filnetlem3  35260  onsucsuccmpi  35323  dissneqlem  36216  icoreunrn  36235  ctbssinf  36282  pibt2  36293  mblfinlem1  36520  ismblfin  36524  sstotbnd2  36637  dochexmidlem4  40329  lcfrlem38  40446  mhpind  41168  ismrcd1  41426  eldioph2lem2  41489  rmxyelqirrOLD  41639  hbt  41862  rngunsnply  41905  iocinico  41951  dmtrcl  42368  rntrcl  42369  trrelsuperrel2dg  42412  restuni5  43802  unirnmapsn  43903  limciccioolb  44327  limcrecl  44335  limcicciooub  44343  stoweidlem50  44756  stoweidlem52  44758  stoweidlem53  44759  stoweidlem57  44763  stoweidlem59  44765  fourierdlem50  44862  fourierdlem103  44915  fourierdlem104  44916  pwsal  45021  sge0iun  45125  sge0isum  45133  meadjuni  45163  omessle  45204  rhmimasubrnglem  46734  zlmodzxzel  47021  lincresunit3  47152  amgmwlem  47839