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

Theorem ssidd 3994
Description: Weakening of ssid 3993. (Contributed by BJ, 1-Sep-2022.)
Assertion
Ref Expression
ssidd (𝜑𝐴𝐴)

Proof of Theorem ssidd
StepHypRef Expression
1 ssid 3993 . 2 𝐴𝐴
21a1i 11 1 (𝜑𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-in 3947  df-ss 3956
This theorem is referenced by:  suppofss1d  7864  suppofss2d  7865  ralxpmap  8454  fissuni  8823  fsuppmptif  8857  fsuppco2  8860  fsuppcor  8861  mapfienlem1  8862  mapfienlem2  8863  cantnfp1lem1  9135  cantnfp1lem3  9137  cantnflem1  9146  htalem  9319  ackbij2lem4  9658  cflim2  9679  fin23lem15  9750  wunex2  10154  swrd0  14015  rtrclreclem2  14413  summolem3  15066  isum  15071  fsumser  15082  fsumcl  15085  flo1  15204  prodmolem3  15282  iprod  15287  iprodn0  15289  fprodss  15297  fprodcl  15301  fprodclf  15341  rpnnen2lem11  15572  eulerthlem2  16114  mremre  16870  catsubcat  17104  yon11  17509  yon12  17510  yon2  17511  yonpropd  17513  oppcyon  17514  yonffth  17529  submid  17970  mulgnncl  18188  mulgnn0cl  18189  mulgcl  18190  subgid  18226  symggen  18534  gsumzcl2  18966  gsumzf1o  18968  gsum2dlem1  19026  gsum2dlem2  19027  gsum2d  19028  gsumxp2  19036  dprdfinv  19077  dmdprdsplitlem  19095  dprd2db  19101  dpjidcl  19116  ablfac1eu  19131  ablfaclem2  19144  gsumdixp  19295  primefld  19520  lcomfsupp  19610  lss1  19646  rlmbas  19903  rlmplusg  19904  rlm0  19905  rlmmulr  19907  rlmsca  19908  rlmsca2  19909  rlmvsca  19910  rlmtopn  19911  rlmds  19912  rnasclassa  20059  mplsubglem  20149  mpllsslem  20150  mplsubrglem  20154  mplcoe1  20181  mplcoe5  20184  mplbas2  20186  evlslem4  20223  psrbagev1  20225  evlslem2  20227  mhpvscacl  20276  regsumsupp  20701  frlmsslsp  20875  frlmup1  20877  mamures  20936  cpmadumatpolylem2  21425  neiptopuni  21673  neiptoptop  21674  restopn2  21720  rncmp  21939  cmpfi  21951  conncn  21969  llyidm  22031  nllyidm  22032  toplly  22033  kgentopon  22081  kgencn2  22100  ptcld  22156  qtopuni  22245  supnfcls  22563  utopbas  22778  metustfbas  23101  rrxcph  23929  rrxmval  23942  rrxdstprj1  23946  evthicc2  23995  volcn  24141  dvres3  24445  dvres3a  24446  dvidlem  24447  dvnadd  24460  dvnres  24462  dvaddbr  24469  dvmulbr  24470  dvcmul  24475  dvcmulf  24476  dvcobr  24477  dvcjbr  24480  dvrec  24486  dveflem  24510  dvef  24511  dvlipcn  24525  dvgt0lem2  24534  lhop1lem  24544  ftc1cn  24574  ftc2  24575  deg1mul3le  24644  coeeulem  24748  dgrcolem1  24797  dgrcolem2  24798  plycpn  24812  dvntaylp  24893  pserdv  24951  pige3ALT  25039  cxpcn2  25259  rlimcnp3  25478  lgamgulmlem2  25540  basellem2  25592  pntrsumo1  26074  pntrsumbnd  26075  nbupgr  27059  nbumgrvtx  27061  nbgr2vtx1edg  27065  cusgrexilem2  27157  ifpsnprss  27337  1pthon2ve  27866  suppovss  30360  offinsupp1  30395  xrsmulgzz  30598  gsummpt2co  30619  symgcom2  30661  pmtrcnelor  30668  tocycfvres1  30685  tocycfvres2  30686  cycpmconjvlem  30716  lindfpropd  30875  rgmoddim  30913  tngdim  30916  matdim  30918  fedgmullem1  30930  mdetpmtr1  30993  pnfneige0  31099  pwsiga  31294  baselcarsg  31469  efmul2picn  31772  reprfz1  31800  breprexplemc  31808  circlemeth  31816  circlevma  31818  circlemethhgt  31819  hgt750lemb  31832  hgt750lema  31833  hgt750leme  31834  tgoldbachgtde  31836  satfsschain  32514  mrsubff1  32664  mrsub0  32666  mrsubccat  32668  mrsubcn  32669  msubff1  32706  mthmpps  32732  trpredpo  32977  wzel  33014  fpr1  33042  nosupbnd1lem1  33111  knoppndvlem6  33759  knoppndv  33776  bj-elpwg  34245  bj-restpw  34283  bj-restb  34285  bj-restuni2  34289  ftc1cnnclem  34851  ftc1cnnc  34852  ftc2nc  34862  areacirclem3  34870  welb  34898  cnresima  34929  rngoidl  35189  1psubclN  36966  cdlemefrs32fva  37422  selvval2lem4  39020  rgspnid  39656  itgpowd  39705  harval3  39788  cnvtrucl0  39868  brfvrtrcld  39963  clsk3nimkb  40274  k0004ss2  40386  extoimad  40399  funfvima2d  40404  mnuprd  40496  dvconstbi  40550  ssinc  41237  ssdec  41238  founiiun  41319  choicefi  41347  islptre  41784  fnlimfvre  41839  addccncf2  42043  fsumcncf  42045  cncfperiod  42046  negcncfg  42048  cncfuni  42053  icccncfext  42054  cncficcgt0  42055  fprodcncf  42068  dvcnre  42084  fperdvper  42087  dvmptresicc  42088  itgsinexplem1  42123  itgcoscmulx  42138  submgmid  43911  rnghmsscmap2  44146  rhmsscmap2  44192  fldhmsubc  44257  fldhmsubcALTV  44275  elbigolo1  44519
  Copyright terms: Public domain W3C validator