Theorem syl6eqss 3880

Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
syl6eqss.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6eqss.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
syl6eqss	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem syl6eqss

Step	Hyp	Ref	Expression
1		syl6eqss.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6eqss.2	. . 3 ⊢ 𝐵 ⊆ 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	1, 3	eqsstrd 3864	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1658   ⊆ wss 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-in 3805  df-ss 3812

This theorem is referenced by:  syl6eqssr  3881  dmxpss  5806  dmsnopss  5848  iotassuni  6102  fvmptss  6539  fvmptss2  6552  fimacnv  6596  funressn  6677  riotassuni  6903  frxp  7551  suppssdm  7572  suppun  7579  suppss  7590  suppssov1  7592  suppss2  7594  suppssfv  7596  wfrlem15  7695  oawordeulem  7901  omwordri  7919  oewordri  7939  fodomr  8380  fipwuni  8601  fipwss  8604  ordtypelem6  8697  inf3lemd  8801  cantnfle  8845  cantnflem2  8864  en2other2  9145  ackbij1lem15  9371  ackbij2lem3  9378  cfub  9386  cflecard  9390  cfle  9391  fin23lem13  9469  fin23lem29  9478  compsscnvlem  9507  itunitc1  9557  fpwwe2lem12  9778  grur1a  9956  uzssz  11988  fsuppmapnn0fiublem  13084  fsuppmapnn0fiub  13085  swrdlend  13718  repswswrd  13900  cshimadifsn  13950  xptrrel  14098  relexpnndm  14158  limsupgle  14585  isercolllem2  14773  isercoll  14775  fsumss  14833  sadcaddlem  15552  sadadd2lem  15554  sadadd3  15556  sadcl  15557  sadaddlem  15561  sadasslem  15565  sadeq  15567  smupvallem  15578  smucl  15579  prmreclem4  15994  prmreclem5  15995  1arith  16002  vdwmc2  16054  vdwlem13  16068  ramz2  16099  strfvss  16245  ressbasss  16295  prdsless  16476  sectss  16764  invss  16773  fullfunc  16918  fthfunc  16919  catccatid  17104  resscatc  17107  catcisolem  17108  catciso  17109  yoniso  17278  gsumpropd2lem  17626  cntzrcl  18110  cntzssv  18111  gsumzmhm  18690  ablfaclem3  18840  lmhmlsp  19408  resspsrbas  19776  resspsrvsca  19779  subrgpsr  19780  mplsubglem  19795  ressmplbas  19817  subrgmpl  19821  mpfrcl  19878  ressply1bas  19959  evpmss  20291  cssss  20392  frlmplusgval  20470  frlmvscafval  20472  uvcresum  20499  scmatlss  20699  cpmatsubgpmat  20895  toponsspwpw  21097  basdif0  21128  ntrss2  21232  ordtbas2  21366  ordtbas  21367  cncls  21449  cmpfi  21582  comppfsc  21706  kgentopon  21712  ptpjpre1  21745  xkoccn  21793  prdstopn  21802  uzfbas  22072  utoptop  22408  utopbas  22409  setsmstopn  22653  restmetu  22745  tngtopn  22824  iccntr  22994  metdstri  23024  pi1xfrcnvlem  23225  cphsubrglem  23346  tcphcph  23405  rrxnm  23559  ovolshftlem1  23675  ovolshft  23677  ovolscalem1  23679  ovolscalem2  23680  ovolsca  23681  uniioombllem2  23749  uniioombllem3a  23750  uniioombllem3  23751  uniioombllem4  23752  uniioombllem6  23754  itgioo  23981  limcnlp  24041  dvbsss  24065  dvcnvrelem1  24179  dvfsumle  24183  dvfsumabs  24185  pserdv  24582  rlimcnp2  25106  fsumharmonic  25151  chpval2  25356  tglnssp  25864  perpln1  26022  perpln2  26023  uhgrspansubgr  26588  clwwlknclwwlkdifnum  27309  ocsh  28697  shsss  28727  speccl  29313  elnlfn  29342  pj3i  29622  sumdmdlem2  29833  fcoinver  29965  ffsrn  30052  ssnnssfz  30096  inftmrel  30279  smatrcl  30407  metidss  30479  fsumcvg4  30541  dya2iocuni  30890  carsgcl  30911  breprexplema  31257  bnj1143  31407  bnj1262  31427  bnj517  31501  kur14lem1  31734  cvmliftmolem2  31810  cvmliftlem15  31826  mrsubrn  31956  msubrn  31972  trpredlem1  32265  bj-ismooredr2  33588  poimirlem30  33983  mblfinlem2  33991  sdclem2  34080  sstotbnd2  34115  isbnd3  34125  lkrlss  35170  pmapssat  35834  diass  37117  diaintclN  37133  dia2dimlem13  37151  dibintclN  37242  lcfrlem25  37642  lcdvbasess  37669  mapdin  37737  diophin  38180  itgocn  38577  relexp0a  38849  frege131d  38897  fsovrfovd  39143  clsk1indlem2  39180  clsk1indlem3  39181  unirestss  40122  fsumsupp0  40605  limsupequzlem  40749  ibliooicc  40981  stoweidlem34  41045  stoweidlem59  41070  etransclem24  41269  caratheodory  41536  ovnhoilem1  41609  hspdifhsp  41624  smfaddlem2  41766  smflimlem1  41773  smflimlem2  41774  smfmullem4  41795  smfsuplem1  41811  rnghmresfn  42810  dfrngc2  42819  rnghmsscmap2  42820  rnghmsscmap  42821  rngchomrnghmresALTV  42843  funcrngcsetc  42845  rhmresfn  42856  dfringc2  42865  rhmsscmap2  42866  rhmsscmap  42867  rhmsscrnghm  42873  funcringcsetc  42882  funcringcsetcALTV2lem9  42891  rngcrescrhm  42932  rhmsubclem1  42933  rhmsubclem4  42936  rngcrescrhmALTV  42950  rhmsubcALTVlem1  42951  ssnn0ssfz  42974  setrec2fun  43334