Theorem sseqtrdi 4045

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  sseqtrrdi  4046  sofld  6208  relrelss  6294  foimacnv  6865  onfununi  8379  hartogslem1  9579  cantnfp1lem3  9717  uniwf  9856  rankeq0b  9897  djuinf  10226  cflecard  10290  fin23lem16  10372  fin23lem41  10389  pwcfsdom  10620  fpwwe2lem12  10679  fpwwe2  10680  canth4  10684  hashbclem  14487  dmtrclfv  15053  zsum  15750  fsumcvg3  15761  incexclem  15868  zprod  15969  ramub1lem1  17059  setsstruct2  17207  imasaddfnlem  17574  imasvscafn  17583  mremre  17648  submre  17649  mreexexlem3d  17690  isacs1i  17701  acsmapd  18611  acsmap2d  18612  ghmqusnsglem1  19310  gsumzoppg  19976  rhmimasubrnglem  20581  subdrgint  20820  primefld  20822  lspsntri  21113  lsppratlem4  21169  lbsextlem3  21179  sraring  21210  evls1maplmhm  22396  distop  23017  elcls  23096  cnpresti  23311  cnprest  23312  cmpcld  23425  cnconn  23445  iunconn  23451  comppfsc  23555  ptuni2  23599  alexsubALTlem3  24072  ustssco  24238  ust0  24243  ustbas2  24249  ustimasn  24252  utopbas  24259  utop2nei  24274  setsmstopn  24505  metustsym  24583  metust  24586  tngtopn  24686  ovoliunlem1  25550  lhop1lem  26066  ig1peu  26228  ig1pdvds  26233  logccv  26719  amgmlem  27047  upgr1e  29144  uspgr1e  29275  shsupcl  31366  shsupunss  31374  shslubi  31413  orthin  31474  h1datomi  31609  mdslj2i  32348  mdslmd1lem1  32353  iundifdifd  32581  difres  32619  fresf1o  32647  suppovss  32695  swrdrndisj  32926  elrgspnlem3  33233  fracf1  33288  idomsubr  33290  nsgmgclem  33418  sradrng  33612  resssra  33616  lsssra  33617  zarcmplem  33841  metideq  33853  hauseqcn  33858  tpr2rico  33872  esumrnmpt2  34048  esumpfinvallem  34054  esum2d  34073  omssubadd  34281  carsggect  34299  omsmeas  34304  orvcelval  34449  signsply0  34544  cvmlift2lem11  35297  cvmlift2lem12  35298  dfon2lem7  35770  filnetlem3  36362  onsucsuccmpi  36425  dissneqlem  37322  icoreunrn  37341  ctbssinf  37388  pibt2  37399  mblfinlem1  37643  ismblfin  37647  sstotbnd2  37760  dochexmidlem4  41445  lcfrlem38  41562  rhmqusspan  42166  mhpind  42580  ismrcd1  42685  eldioph2lem2  42748  rmxyelqirrOLD  42898  hbt  43118  rngunsnply  43157  iocinico  43200  dmtrcl  43616  rntrcl  43617  trrelsuperrel2dg  43660  restuni5  45062  unirnmapsn  45156  limciccioolb  45576  limcrecl  45584  limcicciooub  45592  stoweidlem50  46005  stoweidlem52  46007  stoweidlem53  46008  stoweidlem57  46012  stoweidlem59  46014  fourierdlem50  46111  fourierdlem103  46164  fourierdlem104  46165  pwsal  46270  sge0iun  46374  sge0isum  46382  meadjuni  46412  omessle  46453  zlmodzxzel  48199  lincresunit3  48326  amgmwlem  49032