Theorem sseqtrdi 3971

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  sseqtrrdi  3972  3sstr3g  3983  sofld  6139  relrelss  6225  foimacnv  6785  onfununi  8267  hartogslem1  9435  cantnfp1lem3  9577  uniwf  9719  rankeq0b  9760  djuinf  10087  cflecard  10151  fin23lem16  10233  fin23lem41  10250  pwcfsdom  10481  fpwwe2lem12  10540  fpwwe2  10541  canth4  10545  hashbclem  14361  dmtrclfv  14927  zsum  15627  fsumcvg3  15638  incexclem  15745  zprod  15846  ramub1lem1  16940  setsstruct2  17087  imasaddfnlem  17434  imasvscafn  17443  mremre  17508  submre  17509  mreexexlem3d  17554  isacs1i  17565  acsmapd  18462  acsmap2d  18463  ghmqusnsglem1  19194  gsumzoppg  19858  rhmimasubrnglem  20482  subdrgint  20720  primefld  20722  lspsntri  21033  lsppratlem4  21089  lbsextlem3  21099  sraring  21122  evls1maplmhm  22293  distop  22911  elcls  22989  cnpresti  23204  cnprest  23205  cmpcld  23318  cnconn  23338  iunconn  23344  comppfsc  23448  ptuni2  23492  alexsubALTlem3  23965  ustssco  24131  ust0  24136  ustbas2  24141  ustimasn  24144  utopbas  24151  utop2nei  24166  setsmstopn  24394  metustsym  24471  metust  24474  tngtopn  24566  ovoliunlem1  25431  lhop1lem  25946  ig1peu  26108  ig1pdvds  26113  logccv  26600  amgmlem  26928  upgr1e  29093  uspgr1e  29224  shsupcl  31320  shsupunss  31328  shslubi  31367  orthin  31428  h1datomi  31563  mdslj2i  32302  mdslmd1lem1  32307  iundifdifd  32543  iunxpssiun1  32550  difres  32582  fresf1o  32615  suppovss  32666  swrdrndisj  32945  elrgspnlem3  33218  fracf1  33280  idomsubr  33282  nsgmgclem  33383  ressply1evls1  33535  sradrng  33615  sraidom  33616  resssra  33620  lsssra  33621  extdgfialglem1  33726  extdgfialglem2  33727  zarcmplem  33915  metideq  33927  hauseqcn  33932  tpr2rico  33946  esumrnmpt2  34102  esumpfinvallem  34108  esum2d  34127  omssubadd  34334  carsggect  34352  omsmeas  34357  orvcelval  34503  signsply0  34585  cvmlift2lem11  35378  cvmlift2lem12  35379  dfon2lem7  35852  filnetlem3  36445  onsucsuccmpi  36508  dissneqlem  37405  icoreunrn  37424  ctbssinf  37471  pibt2  37482  mblfinlem1  37717  ismblfin  37721  sstotbnd2  37834  dochexmidlem4  41582  lcfrlem38  41699  rhmqusspan  42298  mhpind  42712  ismrcd1  42815  eldioph2lem2  42878  hbt  43247  rngunsnply  43286  iocinico  43329  dmtrcl  43744  rntrcl  43745  trrelsuperrel2dg  43788  restuni5  45244  unirnmapsn  45335  limciccioolb  45745  limcrecl  45753  limcicciooub  45759  stoweidlem50  46172  stoweidlem52  46174  stoweidlem53  46175  stoweidlem57  46179  stoweidlem59  46181  fourierdlem50  46278  fourierdlem103  46331  fourierdlem104  46332  pwsal  46437  sge0iun  46541  sge0isum  46549  meadjuni  46579  omessle  46620  uhgrimprop  48016  zlmodzxzel  48479  lincresunit3  48606  amgmwlem  49927