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

Theorem syl6eqss 3688
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 3672 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  syl6eqssr  3689  dmxpss  5600  dmsnopss  5643  iotassuni  5905  fvmptss  6331  fvmptss2  6343  fimacnv  6387  funressn  6466  riotassuni  6688  frxp  7332  suppssdm  7353  suppun  7360  suppss  7370  suppssov1  7372  suppss2  7374  suppssfv  7376  wfrlem15  7474  oawordeulem  7679  omwordri  7697  oewordri  7717  fodomr  8152  fipwuni  8373  fipwss  8376  ordtypelem6  8469  inf3lemd  8562  cantnfle  8606  cantnflem2  8625  en2other2  8870  ackbij1lem15  9094  ackbij2lem3  9101  cfub  9109  cflecard  9113  cfle  9114  fin23lem13  9192  fin23lem29  9201  compsscnvlem  9230  itunitc1  9280  fpwwe2lem12  9501  grur1a  9679  uzssz  11745  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  swrdlend  13477  repswswrd  13577  cshimadifsn  13621  xptrrel  13765  relexpnndm  13825  limsupgle  14252  isercolllem2  14440  isercoll  14442  fsumss  14500  sadcaddlem  15226  sadadd2lem  15228  sadadd3  15230  sadcl  15231  sadaddlem  15235  sadasslem  15239  sadeq  15241  smupvallem  15252  smucl  15253  prmreclem4  15670  prmreclem5  15671  1arith  15678  vdwmc2  15730  vdwlem13  15744  ramz2  15775  strfvss  15927  ressbasss  15979  prdsless  16170  sectss  16459  invss  16468  fullfunc  16613  fthfunc  16614  catccatid  16799  resscatc  16802  catcisolem  16803  catciso  16804  yoniso  16972  gsumpropd2lem  17320  cntzrcl  17806  cntzssv  17807  gsumzmhm  18383  ablfaclem3  18532  lmhmlsp  19097  resspsrbas  19463  resspsrvsca  19466  subrgpsr  19467  mplsubglem  19482  ressmplbas  19504  subrgmpl  19508  mpfrcl  19566  ressply1bas  19647  evpmss  19980  cssss  20077  frlmplusgval  20155  frlmvscafval  20157  uvcresum  20180  scmatlss  20379  cpmatsubgpmat  20573  toponsspwpw  20774  basdif0  20805  ntrss2  20909  ordtbas2  21043  ordtbas  21044  cncls  21126  cmpfi  21259  comppfsc  21383  kgentopon  21389  ptpjpre1  21422  xkoccn  21470  prdstopn  21479  uzfbas  21749  utoptop  22085  utopbas  22086  setsmstopn  22330  restmetu  22422  tngtopn  22501  iccntr  22671  metdstri  22701  pi1xfrcnvlem  22902  cphsubrglem  23023  tchcph  23082  rrxnm  23225  ovolshftlem1  23323  ovolshft  23325  ovolscalem1  23327  ovolscalem2  23328  ovolsca  23329  uniioombllem2  23397  uniioombllem3a  23398  uniioombllem3  23399  uniioombllem4  23400  uniioombllem6  23402  itgioo  23627  limcnlp  23687  dvbsss  23711  dvcnvrelem1  23825  dvfsumle  23829  dvfsumabs  23831  pserdv  24228  rlimcnp2  24738  fsumharmonic  24783  chpval2  24988  tglnssp  25492  perpln1  25650  perpln2  25651  uhgrspansubgr  26228  clwwlknclwwlkdifnum  26946  ocsh  28270  shsss  28300  speccl  28886  elnlfn  28915  pj3i  29195  sumdmdlem2  29406  fcoinver  29544  ffsrn  29632  ssnnssfz  29677  inftmrel  29862  smatrcl  29990  metidss  30062  fsumcvg4  30124  dya2iocuni  30473  carsgcl  30494  breprexplema  30836  bnj1143  30987  bnj1262  31007  bnj517  31081  kur14lem1  31314  cvmliftmolem2  31390  cvmliftlem15  31406  mrsubrn  31536  msubrn  31552  trpredlem1  31851  bj-ismooredr2  33190  poimirlem30  33569  mblfinlem2  33577  sdclem2  33668  sstotbnd2  33703  isbnd3  33713  lkrlss  34700  pmapssat  35363  diass  36648  diaintclN  36664  dia2dimlem13  36682  dibintclN  36773  lcfrlem25  37173  lcdvbasess  37200  mapdin  37268  diophin  37653  itgocn  38051  relexp0a  38325  frege131d  38373  fsovrfovd  38620  clsk1indlem2  38657  clsk1indlem3  38658  unirestss  39621  fsumsupp0  40128  limsupequzlem  40272  ibliooicc  40505  stoweidlem34  40569  stoweidlem59  40594  etransclem24  40793  caratheodory  41063  ovnhoilem1  41136  hspdifhsp  41151  smfaddlem2  41293  smflimlem1  41300  smflimlem2  41301  smfmullem4  41322  smfsuplem1  41338  rnghmresfn  42288  rnghmsscmap2  42298  rnghmsscmap  42299  rngchomrnghmresALTV  42321  funcrngcsetc  42323  rhmresfn  42334  dfringc2  42343  rhmsscmap2  42344  rhmsscmap  42345  rhmsscrnghm  42351  funcringcsetc  42360  funcringcsetcALTV2lem9  42369  rngcrescrhm  42410  rhmsubclem1  42411  rhmsubclem4  42414  rngcrescrhmALTV  42428  rhmsubcALTVlem1  42429  ssnn0ssfz  42452  setrec2fun  42764
  Copyright terms: Public domain W3C validator