MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6eqss Structured version   Visualization version   GIF version

Theorem syl6eqss 3618
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
StepHypRef Expression
1 syl6eqss.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6eqss.2 . . 3 𝐵𝐶
32a1i 11 . 2 (𝜑𝐵𝐶)
41, 3eqsstrd 3602 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  syl6eqssr  3619  dmxpss  5484  dmsnopss  5525  iotassuni  5784  fvmptss  6201  fvmptss2  6212  fimacnv  6255  funressn  6331  riotassuni  6547  frxp  7174  suppssdm  7195  suppun  7202  suppss  7212  suppssov1  7214  suppss2  7216  suppssfv  7218  wfrlem15  7316  oawordeulem  7521  omwordri  7539  oewordri  7559  fodomr  7996  fipwuni  8215  fipwss  8218  ordtypelem6  8311  inf3lemd  8407  cantnfle  8451  cantnflem2  8470  en2other2  8715  ackbij1lem15  8939  ackbij2lem3  8946  cfub  8954  cflecard  8958  cfle  8959  fin23lem13  9037  fin23lem29  9046  compsscnvlem  9075  itunitc1  9125  fpwwe2lem12  9342  grur1a  9520  uzssz  11583  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  swrdlend  13283  repswswrd  13382  cshimadifsn  13426  xptrrel  13567  relexpnndm  13629  limsupgle  14056  isercolllem2  14244  isercoll  14246  fsumss  14303  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  sadcl  15022  sadaddlem  15026  sadasslem  15030  sadeq  15032  smupvallem  15043  smucl  15044  prmreclem4  15461  prmreclem5  15462  1arith  15469  vdwmc2  15521  vdwlem13  15535  ramz2  15566  strfvss  15713  ressbasss  15759  prdsless  15946  sectss  16235  invss  16244  fullfunc  16389  fthfunc  16390  catccatid  16575  resscatc  16578  catcisolem  16579  catciso  16580  yoniso  16748  gsumpropd2lem  17096  cntzrcl  17583  cntzssv  17584  gsumzmhm  18160  ablfaclem3  18309  lmhmlsp  18870  resspsrbas  19236  resspsrvsca  19239  subrgpsr  19240  mplsubglem  19255  ressmplbas  19277  subrgmpl  19281  mpfrcl  19339  ressply1bas  19420  evpmss  19751  cssss  19848  frlmplusgval  19926  frlmvscafval  19928  uvcresum  19951  scmatlss  20150  cpmatsubgpmat  20344  basdif0  20568  ntrss2  20671  ordtbas2  20805  ordtbas  20806  cncls  20888  cmpfi  21021  comppfsc  21145  kgentopon  21151  ptpjpre1  21184  xkoccn  21232  prdstopn  21241  uzfbas  21512  utoptop  21848  utopbas  21849  setsmstopn  22093  restmetu  22185  tngtopn  22264  iccntr  22432  metdstri  22462  pi1xfrcnvlem  22664  cphsubrglem  22785  tchcph  22844  rrxnm  22987  ovolshftlem1  23084  ovolshft  23086  ovolscalem1  23088  ovolscalem2  23089  ovolsca  23090  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem6  23162  itgioo  23388  limcnlp  23448  dvbsss  23472  dvcnvrelem1  23584  dvfsumle  23588  dvfsumabs  23590  pserdv  23987  rlimcnp2  24493  fsumharmonic  24538  chpval2  24743  tglnssp  25247  perpln1  25405  perpln2  25406  nbgrassvt  25962  clwwlksswrd  26305  ocsh  27526  shsss  27556  speccl  28142  elnlfn  28171  pj3i  28451  sumdmdlem2  28662  fcoinver  28798  ffsrn  28892  ssnnssfz  28937  inftmrel  29065  smatrcl  29190  metidss  29262  fsumcvg4  29324  dya2iocuni  29672  carsgcl  29693  bnj1143  30115  bnj1262  30135  bnj517  30209  kur14lem1  30442  cvmliftmolem2  30518  cvmliftlem15  30534  mrsubrn  30664  msubrn  30680  trpredlem1  30971  bj-toponss  32241  poimirlem30  32609  mblfinlem2  32617  sdclem2  32708  sstotbnd2  32743  isbnd3  32753  lkrlss  33400  pmapssat  34063  diass  35349  diaintclN  35365  dia2dimlem13  35383  dibintclN  35474  lcfrlem25  35874  lcdvbasess  35901  mapdin  35969  diophin  36354  itgocn  36753  relexp0a  37027  frege131d  37075  fsovrfovd  37323  clsk1indlem2  37360  clsk1indlem3  37361  unirestss  38339  fsumsupp0  38645  ibliooicc  38863  stoweidlem34  38927  stoweidlem59  38952  etransclem24  39151  caratheodory  39418  ovnhoilem1  39491  hspdifhsp  39506  smfaddlem2  39650  smflimlem1  39657  smflimlem2  39658  smfmullem4  39679  uhgrspansubgr  40515  rnghmresfn  41755  rnghmsscmap2  41765  rnghmsscmap  41766  rngchomrnghmresALTV  41788  funcrngcsetc  41790  rhmresfn  41801  dfringc2  41810  rhmsscmap2  41811  rhmsscmap  41812  rhmsscrnghm  41818  funcringcsetc  41827  funcringcsetcALTV2lem9  41836  rngcrescrhm  41877  rhmsubclem1  41878  rhmsubclem4  41881  rngcrescrhmALTV  41896  rhmsubcALTVlem1  41897  ssnn0ssfz  41920  setrec2fun  42238
  Copyright terms: Public domain W3C validator