Theorem sseqtrdi 3978

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  sseqtrrdi  3979  3sstr3g  3990  sofld  6140  relrelss  6225  foimacnv  6785  onfununi  8271  hartogslem1  9453  cantnfp1lem3  9595  uniwf  9734  rankeq0b  9775  djuinf  10102  cflecard  10166  fin23lem16  10248  fin23lem41  10265  pwcfsdom  10496  fpwwe2lem12  10555  fpwwe2  10556  canth4  10560  hashbclem  14377  dmtrclfv  14943  zsum  15643  fsumcvg3  15654  incexclem  15761  zprod  15862  ramub1lem1  16956  setsstruct2  17103  imasaddfnlem  17450  imasvscafn  17459  mremre  17524  submre  17525  mreexexlem3d  17570  isacs1i  17581  acsmapd  18478  acsmap2d  18479  ghmqusnsglem1  19177  gsumzoppg  19841  rhmimasubrnglem  20468  subdrgint  20706  primefld  20708  lspsntri  21019  lsppratlem4  21075  lbsextlem3  21085  sraring  21108  evls1maplmhm  22280  distop  22898  elcls  22976  cnpresti  23191  cnprest  23192  cmpcld  23305  cnconn  23325  iunconn  23331  comppfsc  23435  ptuni2  23479  alexsubALTlem3  23952  ustssco  24118  ust0  24123  ustbas2  24129  ustimasn  24132  utopbas  24139  utop2nei  24154  setsmstopn  24382  metustsym  24459  metust  24462  tngtopn  24554  ovoliunlem1  25419  lhop1lem  25934  ig1peu  26096  ig1pdvds  26101  logccv  26588  amgmlem  26916  upgr1e  29076  uspgr1e  29207  shsupcl  31300  shsupunss  31308  shslubi  31347  orthin  31408  h1datomi  31543  mdslj2i  32282  mdslmd1lem1  32287  iundifdifd  32523  iunxpssiun1  32530  difres  32562  fresf1o  32588  suppovss  32637  swrdrndisj  32912  elrgspnlem3  33194  fracf1  33256  idomsubr  33258  nsgmgclem  33358  ressply1evls1  33510  sradrng  33554  sraidom  33555  resssra  33559  lsssra  33560  zarcmplem  33847  metideq  33859  hauseqcn  33864  tpr2rico  33878  esumrnmpt2  34034  esumpfinvallem  34040  esum2d  34059  omssubadd  34267  carsggect  34285  omsmeas  34290  orvcelval  34436  signsply0  34518  cvmlift2lem11  35285  cvmlift2lem12  35286  dfon2lem7  35762  filnetlem3  36353  onsucsuccmpi  36416  dissneqlem  37313  icoreunrn  37332  ctbssinf  37379  pibt2  37390  mblfinlem1  37636  ismblfin  37640  sstotbnd2  37753  dochexmidlem4  41442  lcfrlem38  41559  rhmqusspan  42158  mhpind  42567  ismrcd1  42671  eldioph2lem2  42734  hbt  43103  rngunsnply  43142  iocinico  43185  dmtrcl  43600  rntrcl  43601  trrelsuperrel2dg  43644  restuni5  45101  unirnmapsn  45192  limciccioolb  45603  limcrecl  45611  limcicciooub  45619  stoweidlem50  46032  stoweidlem52  46034  stoweidlem53  46035  stoweidlem57  46039  stoweidlem59  46041  fourierdlem50  46138  fourierdlem103  46191  fourierdlem104  46192  pwsal  46297  sge0iun  46401  sge0isum  46409  meadjuni  46439  omessle  46480  uhgrimprop  47877  zlmodzxzel  48340  lincresunit3  48467  amgmwlem  49788