Theorem sseqtrdi 3953

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  sseqtrrdi  3954  3sstr3g  3965  sofld  6192  relrelss  6294  foimacnv  6867  onfununi  8380  hartogslem1  9566  cantnfp1lem3  9711  uniwf  9858  rankeq0b  9906  djuinf  10297  cflecard  10360  fin23lem16  10443  fin23lem41  10460  pwcfsdom  10698  fpwwe2lem12  10757  fpwwe2  10758  canth4  10762  hashbclem  14627  dmtrclfv  15203  zsum  15916  fsumcvg3  15927  incexclem  16037  zprod  16136  ramub1lem1  17236  setsstruct2  17384  imasaddfnlem  17732  imasvscafn  17741  mremre  17806  submre  17807  mreexexlem3d  17852  isacs1i  17863  acsmapd  18760  acsmap2d  18761  ghmqusnsglem1  19527  gsumzoppg  20191  rhmimasubrnglem  20850  subdrgint  21093  primefld  21095  lspsntri  21405  lsppratlem4  21461  lbsextlem3  21471  sraring  21494  evls1maplmhm  22728  distop  23346  elcls  23424  cnpresti  23639  cnprest  23640  cmpcld  23753  cnconn  23773  iunconn  23779  comppfsc  23884  ptuni2  23928  alexsubALTlem3  24401  ustssco  24567  ust0  24572  ustbas2  24577  ustimasn  24580  utopbas  24587  utop2nei  24602  setsmstopn  24830  metustsym  24907  metust  24910  tngtopn  25002  ovoliunlem1  25856  lhop1lem  26366  ig1peu  26526  ig1pdvds  26531  logccv  27024  amgmlem  27350  upgr1e  29724  uspgr1e  29858  shsupcl  31973  shsupunss  31981  shslubi  32020  orthin  32081  h1datomi  32216  mdslj2i  32955  mdslmd1lem1  32960  iundifdifd  33231  iunxpssiun1  33237  difres  33269  fresf1o  33300  suppovss  33348  swrdrndisj  33591  elrgspnlem3  33881  fracf1  33953  idomsubr  33955  nsgmgclem  34046  ressply1evls1  34180  sradrng  34297  sraidom  34298  resssra  34302  lsssra  34303  extdgfialglem1  34407  extdgfialglem2  34408  zarcmplem  34596  metideq  34608  hauseqcn  34613  tpr2rico  34627  esumrnmpt2  34783  esumpfinvallem  34789  esum2d  34808  omssubadd  35015  carsggect  35033  omsmeas  35038  orvcelval  35184  signsply0  35263  cvmlift2lem11  36258  cvmlift2lem12  36259  dfon2lem7  36742  filnetlem3  37359  onsucsuccmpi  37422  dissneqlem  38468  icoreunrn  38487  ctbssinf  38534  pibt2  38545  mblfinlem1  38780  ismblfin  38784  sstotbnd2  38911  dochexmidlem4  42723  lcfrlem38  42840  rhmqusspan  43438  mhpind  43826  ismrcd1  43913  eldioph2lem2  43976  hbt  44335  rngunsnply  44374  iocinico  44417  dmtrcl  44830  rntrcl  44831  trrelsuperrel2dg  44874  restuni5  46353  unirnmapsn  46442  limciccioolb  46848  limcrecl  46856  limcicciooub  46862  stoweidlem50  47275  stoweidlem52  47277  stoweidlem53  47278  stoweidlem57  47282  stoweidlem59  47284  fourierdlem50  47381  fourierdlem103  47434  fourierdlem104  47435  pwsal  47540  sge0iun  47644  sge0isum  47652  meadjuni  47682  omessle  47723  uhgrimprop  49205  zlmodzxzel  49682  lincresunit3  49808  amgmwlem  51299