Theorem syl6eqss 3874

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 3858	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1601   ⊆ wss 3792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-in 3799  df-ss 3806

This theorem is referenced by:  syl6eqssr  3875  dmxpss  5819  dmsnopss  5861  iotassuni  6115  fvmptss  6553  fvmptss2  6566  fimacnv  6611  funressn  6692  riotassuni  6920  frxp  7568  suppssdm  7589  suppun  7596  suppss  7607  suppssov1  7609  suppss2  7611  suppssfv  7613  wfrlem15  7712  oawordeulem  7918  omwordri  7936  oewordri  7956  fodomr  8399  fipwuni  8620  fipwss  8623  ordtypelem6  8717  inf3lemd  8821  cantnfle  8865  cantnflem2  8884  en2other2  9165  ackbij1lem15  9391  ackbij2lem3  9398  cfub  9406  cflecard  9410  cfle  9411  fin23lem13  9489  fin23lem29  9498  compsscnvlem  9527  itunitc1  9577  fpwwe2lem12  9798  grur1a  9976  uzssz  12012  fsuppmapnn0fiublem  13108  fsuppmapnn0fiub  13109  swrdlend  13748  repswswrd  13930  cshimadifsn  13980  xptrrel  14128  relexpnndm  14188  limsupgle  14616  isercolllem2  14804  isercolllem3  14805  isercoll  14806  fsumss  14863  sadcaddlem  15585  sadadd2lem  15587  sadadd3  15589  sadcl  15590  sadaddlem  15594  sadasslem  15598  sadeq  15600  smupvallem  15611  smucl  15612  prmreclem4  16027  prmreclem5  16028  1arith  16035  vdwmc2  16087  vdwlem13  16101  ramz2  16132  strfvss  16278  ressbasss  16328  prdsless  16509  sectss  16797  invss  16806  fullfunc  16951  fthfunc  16952  catccatid  17137  resscatc  17140  catcisolem  17141  catciso  17142  yoniso  17311  gsumpropd2lem  17659  cntzrcl  18143  cntzssv  18144  gsumzmhm  18723  ablfaclem3  18873  lmhmlsp  19444  resspsrbas  19812  resspsrvsca  19815  subrgpsr  19816  mplsubglem  19831  ressmplbas  19853  subrgmpl  19857  mpfrcl  19914  ressply1bas  19995  evpmss  20327  cssss  20428  frlmplusgval  20507  frlmvscafval  20509  uvcresum  20536  scmatlss  20736  cpmatsubgpmat  20932  toponsspwpw  21134  basdif0  21165  ntrss2  21269  ordtbas2  21403  ordtbas  21404  cncls  21486  cmpfi  21620  comppfsc  21744  kgentopon  21750  ptpjpre1  21783  xkoccn  21831  prdstopn  21840  uzfbas  22110  utoptop  22446  utopbas  22447  setsmstopn  22691  restmetu  22783  tngtopn  22862  iccntr  23032  metdstri  23062  pi1xfrcnvlem  23263  cphsubrglem  23384  tcphcph  23443  rrxnm  23597  ovolshftlem1  23713  ovolshft  23715  ovolscalem1  23717  ovolscalem2  23718  ovolsca  23719  uniioombllem2  23787  uniioombllem3a  23788  uniioombllem3  23789  uniioombllem4  23790  uniioombllem6  23792  itgioo  24019  limcnlp  24079  dvbsss  24103  dvcnvrelem1  24217  dvfsumle  24221  dvfsumabs  24223  pserdv  24620  rlimcnp2  25145  fsumharmonic  25190  chpval2  25395  tglnssp  25903  perpln1  26061  perpln2  26062  uhgrspansubgr  26638  clwwlknclwwlkdifnum  27360  ocsh  28714  shsss  28744  speccl  29330  elnlfn  29359  pj3i  29639  sumdmdlem2  29850  fcoinver  29981  ffsrn  30070  ssnnssfz  30113  inftmrel  30296  smatrcl  30460  metidss  30532  fsumcvg4  30594  dya2iocuni  30943  carsgcl  30964  breprexplema  31310  bnj1143  31460  bnj1262  31480  bnj517  31554  kur14lem1  31787  cvmliftmolem2  31863  cvmliftlem15  31879  mrsubrn  32009  msubrn  32025  trpredlem1  32315  bj-ismooredr2  33638  poimirlem30  34065  mblfinlem2  34073  sdclem2  34162  sstotbnd2  34197  isbnd3  34207  lkrlss  35249  pmapssat  35913  diass  37196  diaintclN  37212  dia2dimlem13  37230  dibintclN  37321  lcfrlem25  37721  lcdvbasess  37748  mapdin  37816  diophin  38296  itgocn  38693  relexp0a  38965  frege131d  39013  fsovrfovd  39259  clsk1indlem2  39296  clsk1indlem3  39297  unirestss  40236  fsumsupp0  40718  limsupequzlem  40862  ibliooicc  41114  stoweidlem34  41178  stoweidlem59  41203  etransclem24  41402  caratheodory  41669  ovnhoilem1  41742  hspdifhsp  41757  smfaddlem2  41899  smflimlem1  41906  smflimlem2  41907  smfmullem4  41928  smfsuplem1  41944  rnghmresfn  42978  dfrngc2  42987  rnghmsscmap2  42988  rnghmsscmap  42989  rngchomrnghmresALTV  43011  funcrngcsetc  43013  rhmresfn  43024  dfringc2  43033  rhmsscmap2  43034  rhmsscmap  43035  rhmsscrnghm  43041  funcringcsetc  43050  funcringcsetcALTV2lem9  43059  rngcrescrhm  43100  rhmsubclem1  43101  rhmsubclem4  43104  rngcrescrhmALTV  43118  rhmsubcALTVlem1  43119  ssnn0ssfz  43142  setrec2fun  43544