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

Theorem syl6eqss 3640
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 3624 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574
This theorem is referenced by:  syl6eqssr  3641  dmxpss  5534  dmsnopss  5576  iotassuni  5836  fvmptss  6259  fvmptss2  6270  fimacnv  6313  funressn  6391  riotassuni  6613  frxp  7247  suppssdm  7268  suppun  7275  suppss  7285  suppssov1  7287  suppss2  7289  suppssfv  7291  wfrlem15  7389  oawordeulem  7594  omwordri  7612  oewordri  7632  fodomr  8071  fipwuni  8292  fipwss  8295  ordtypelem6  8388  inf3lemd  8484  cantnfle  8528  cantnflem2  8547  en2other2  8792  ackbij1lem15  9016  ackbij2lem3  9023  cfub  9031  cflecard  9035  cfle  9036  fin23lem13  9114  fin23lem29  9123  compsscnvlem  9152  itunitc1  9202  fpwwe2lem12  9423  grur1a  9601  uzssz  11667  fsuppmapnn0fiublem  12745  fsuppmapnn0fiub  12746  fsuppmapnn0fiubOLD  12747  swrdlend  13385  repswswrd  13484  cshimadifsn  13528  xptrrel  13669  relexpnndm  13731  limsupgle  14158  isercolllem2  14346  isercoll  14348  fsumss  14405  sadcaddlem  15122  sadadd2lem  15124  sadadd3  15126  sadcl  15127  sadaddlem  15131  sadasslem  15135  sadeq  15137  smupvallem  15148  smucl  15149  prmreclem4  15566  prmreclem5  15567  1arith  15574  vdwmc2  15626  vdwlem13  15640  ramz2  15671  strfvss  15821  ressbasss  15872  prdsless  16063  sectss  16352  invss  16361  fullfunc  16506  fthfunc  16507  catccatid  16692  resscatc  16695  catcisolem  16696  catciso  16697  yoniso  16865  gsumpropd2lem  17213  cntzrcl  17700  cntzssv  17701  gsumzmhm  18277  ablfaclem3  18426  lmhmlsp  18989  resspsrbas  19355  resspsrvsca  19358  subrgpsr  19359  mplsubglem  19374  ressmplbas  19396  subrgmpl  19400  mpfrcl  19458  ressply1bas  19539  evpmss  19872  cssss  19969  frlmplusgval  20047  frlmvscafval  20049  uvcresum  20072  scmatlss  20271  cpmatsubgpmat  20465  toponsspwpw  20666  basdif0  20697  ntrss2  20801  ordtbas2  20935  ordtbas  20936  cncls  21018  cmpfi  21151  comppfsc  21275  kgentopon  21281  ptpjpre1  21314  xkoccn  21362  prdstopn  21371  uzfbas  21642  utoptop  21978  utopbas  21979  setsmstopn  22223  restmetu  22315  tngtopn  22394  iccntr  22564  metdstri  22594  pi1xfrcnvlem  22796  cphsubrglem  22917  tchcph  22976  rrxnm  23119  ovolshftlem1  23217  ovolshft  23219  ovolscalem1  23221  ovolscalem2  23222  ovolsca  23223  uniioombllem2  23291  uniioombllem3a  23292  uniioombllem3  23293  uniioombllem4  23294  uniioombllem6  23296  itgioo  23522  limcnlp  23582  dvbsss  23606  dvcnvrelem1  23718  dvfsumle  23722  dvfsumabs  23724  pserdv  24121  rlimcnp2  24627  fsumharmonic  24672  chpval2  24877  tglnssp  25381  perpln1  25539  perpln2  25540  uhgrspansubgr  26110  ocsh  28030  shsss  28060  speccl  28646  elnlfn  28675  pj3i  28955  sumdmdlem2  29166  fcoinver  29302  ffsrn  29388  ssnnssfz  29432  inftmrel  29561  smatrcl  29686  metidss  29758  fsumcvg4  29820  dya2iocuni  30168  carsgcl  30189  bnj1143  30622  bnj1262  30642  bnj517  30716  kur14lem1  30949  cvmliftmolem2  31025  cvmliftlem15  31041  mrsubrn  31171  msubrn  31187  trpredlem1  31481  poimirlem30  33110  mblfinlem2  33118  sdclem2  33209  sstotbnd2  33244  isbnd3  33254  lkrlss  33901  pmapssat  34564  diass  35850  diaintclN  35866  dia2dimlem13  35884  dibintclN  35975  lcfrlem25  36375  lcdvbasess  36402  mapdin  36470  diophin  36855  itgocn  37254  relexp0a  37528  frege131d  37576  fsovrfovd  37824  clsk1indlem2  37861  clsk1indlem3  37862  unirestss  38832  fsumsupp0  39246  limsupequzlem  39390  ibliooicc  39524  stoweidlem34  39588  stoweidlem59  39613  etransclem24  39812  caratheodory  40079  ovnhoilem1  40152  hspdifhsp  40167  smfaddlem2  40309  smflimlem1  40316  smflimlem2  40317  smfmullem4  40338  smfsuplem1  40354  rnghmresfn  41281  rnghmsscmap2  41291  rnghmsscmap  41292  rngchomrnghmresALTV  41314  funcrngcsetc  41316  rhmresfn  41327  dfringc2  41336  rhmsscmap2  41337  rhmsscmap  41338  rhmsscrnghm  41344  funcringcsetc  41353  funcringcsetcALTV2lem9  41362  rngcrescrhm  41403  rhmsubclem1  41404  rhmsubclem4  41407  rngcrescrhmALTV  41421  rhmsubcALTVlem1  41422  ssnn0ssfz  41445  setrec2fun  41762
  Copyright terms: Public domain W3C validator