Theorem sseqtrdi 3972

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  sseqtrrdi  3973  sofld  6095  relrelss  6180  foimacnv  6742  onfununi  8181  hartogslem1  9310  cantnfp1lem3  9447  uniwf  9586  rankeq0b  9627  djuinf  9953  cflecard  10018  fin23lem16  10100  fin23lem41  10117  pwcfsdom  10348  fpwwe2lem12  10407  fpwwe2  10408  canth4  10412  hashbclem  14173  dmtrclfv  14738  zsum  15439  fsumcvg3  15450  incexclem  15557  zprod  15656  ramub1lem1  16736  setsstruct2  16884  imasaddfnlem  17248  imasvscafn  17257  mremre  17322  submre  17323  mreexexlem3d  17364  isacs1i  17375  acsmapd  18281  acsmap2d  18282  gsumzoppg  19554  subdrgint  20080  primefld  20082  lspsntri  20368  lsppratlem4  20421  lbsextlem3  20431  distop  22154  elcls  22233  cnpresti  22448  cnprest  22449  cmpcld  22562  cnconn  22582  iunconn  22588  comppfsc  22692  ptuni2  22736  alexsubALTlem3  23209  ustssco  23375  ust0  23380  ustbas2  23386  ustimasn  23389  utopbas  23396  utop2nei  23411  setsmstopn  23642  metustsym  23720  metust  23723  tngtopn  23823  ovoliunlem1  24675  lhop1lem  25186  ig1peu  25345  ig1pdvds  25350  logccv  25827  amgmlem  26148  upgr1e  27492  uspgr1e  27620  shsupcl  29709  shsupunss  29717  shslubi  29756  orthin  29817  h1datomi  29952  mdslj2i  30691  mdslmd1lem1  30696  iundifdifd  30910  difres  30948  fresf1o  30975  suppovss  31026  swrdrndisj  31238  nsgmgclem  31605  sraring  31681  sradrng  31682  zarcmplem  31840  metideq  31852  hauseqcn  31857  tpr2rico  31871  esumrnmpt2  32045  esumpfinvallem  32051  esum2d  32070  omssubadd  32276  carsggect  32294  omsmeas  32299  orvcelval  32444  signsply0  32539  cvmlift2lem11  33284  cvmlift2lem12  33285  dfon2lem7  33774  filnetlem3  34578  onsucsuccmpi  34641  dissneqlem  35520  icoreunrn  35539  ctbssinf  35586  pibt2  35597  mblfinlem1  35823  ismblfin  35827  sstotbnd2  35941  dochexmidlem4  39484  lcfrlem38  39601  mhpind  40290  ismrcd1  40527  eldioph2lem2  40590  rmxyelqirr  40739  hbt  40962  rngunsnply  41005  iocinico  41050  dmtrcl  41242  rntrcl  41243  trrelsuperrel2dg  41286  restuni5  42679  unirnmapsn  42761  limciccioolb  43169  limcrecl  43177  limcicciooub  43185  stoweidlem50  43598  stoweidlem52  43600  stoweidlem53  43601  stoweidlem57  43605  stoweidlem59  43607  fourierdlem50  43704  fourierdlem103  43757  fourierdlem104  43758  pwsal  43863  sge0iun  43964  sge0isum  43972  meadjuni  44002  omessle  44043  zlmodzxzel  45702  lincresunit3  45833  amgmwlem  46517