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

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

Proof of Theorem ssidd
StepHypRef Expression
1 ssid 3819 . 2 𝐴𝐴
21a1i 11 1 (𝜑𝐴𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-in 3776  df-ss 3783
This theorem is referenced by:  suppofss1d  7570  suppofss2d  7571  ralxpmap  8147  fissuni  8513  fsuppmptif  8547  fsuppco2  8550  fsuppcor  8551  mapfienlem1  8552  mapfienlem2  8553  cantnfp1lem3  8827  cantnflem1  8836  htalem  9009  ackbij2lem4  9352  cflim2  9373  fin23lem15  9444  wunex2  9848  rtrclreclem2  14140  summolem3  14786  isum  14791  fsumser  14802  fsumcl  14805  flo1  14924  prodmolem3  15000  iprod  15005  iprodn0  15007  fprodss  15015  fprodcl  15019  fprodclf  15059  rpnnen2lem11  15289  eulerthlem2  15820  mremre  16579  catsubcat  16813  yon11  17219  yon12  17220  yon2  17221  yonpropd  17223  oppcyon  17224  yonffth  17239  submid  17666  mulgnncl  17872  mulgnn0cl  17873  mulgcl  17874  subgid  17909  symggen  18202  gsumzcl2  18626  gsumzf1o  18628  gsum2dlem1  18684  gsum2dlem2  18685  gsum2d  18686  dprdfinv  18734  dmdprdsplitlem  18752  dprd2db  18758  dpjidcl  18773  ablfac1eu  18788  ablfaclem2  18801  gsumdixp  18925  lcomfsupp  19221  lss1  19257  rlmbas  19518  rlmplusg  19519  rlm0  19520  rlmmulr  19522  rlmsca  19523  rlmsca2  19524  rlmvsca  19525  rlmtopn  19526  rlmds  19527  mplsubglem  19757  mpllsslem  19758  mplsubrglem  19762  mplcoe1  19788  mplcoe5  19791  mplbas2  19793  evlslem4  19830  psrbagev1  19832  evlslem2  19834  regsumsupp  20291  frlmsslsp  20460  frlmup1  20462  mamures  20521  cpmadumatpolylem2  21015  neiptopuni  21263  neiptoptop  21264  restopn2  21310  rncmp  21528  cmpfi  21540  conncn  21558  llyidm  21620  nllyidm  21621  toplly  21622  kgentopon  21670  kgencn2  21689  ptcld  21745  qtopuni  21834  supnfcls  22152  utopbas  22367  metustfbas  22690  rrxcph  23518  rrxmval  23527  rrxdstprj1  23531  evthicc2  23568  volcn  23714  dvres3  24018  dvres3a  24019  dvidlem  24020  dvnadd  24033  dvnres  24035  dvaddbr  24042  dvmulbr  24043  dvcmul  24048  dvcmulf  24049  dvcobr  24050  dvcjbr  24053  dvrec  24059  dveflem  24083  dvef  24084  dvlipcn  24098  dvgt0lem2  24107  lhop1lem  24117  ftc1cn  24147  ftc2  24148  deg1mul3le  24217  coeeulem  24321  dgrcolem1  24370  dgrcolem2  24371  plycpn  24385  dvntaylp  24466  pserdv  24524  pige3  24611  cxpcn2  24831  rlimcnp3  25046  lgamgulmlem2  25108  basellem2  25160  pntrsumo1  25606  pntrsumbnd  25607  nbupgr  26582  nbumgrvtx  26584  nbgr2vtx1edg  26588  cusgrexilem2  26692  ifpsnprss  26872  1pthon2ve  27498  xrsmulgzz  30194  gsummpt2co  30296  mdetpmtr1  30405  pnfneige0  30513  pwsiga  30709  baselcarsg  30884  efmul2picn  31194  reprfz1  31222  breprexplemc  31230  circlemeth  31238  circlevma  31240  circlemethhgt  31241  hgt750lemb  31254  hgt750lema  31255  hgt750leme  31256  tgoldbachgtde  31258  mrsubff1  31928  mrsub0  31930  mrsubccat  31932  mrsubcn  31933  msubff1  31970  mthmpps  31996  trpredpo  32247  wzel  32282  nosupbnd1lem1  32367  knoppndvlem6  33016  knoppndv  33033  bj-restpw  33538  bj-restb  33540  bj-restuni2  33544  ftc1cnnclem  33971  ftc1cnnc  33972  ftc2nc  33982  areacirclem3  33990  welb  34019  cnresima  34050  rngoidl  34310  1psubclN  35965  cdlemefrs32fva  36421  rgspnid  38527  itgpowd  38584  cnvtrucl0  38714  brfvrtrcld  38809  clsk3nimkb  39120  k0004ss2  39232  wfximgfd  39245  extoimad  39246  funfvima2d  39251  dvconstbi  39315  ssinc  40023  ssdec  40024  founiiun  40115  choicefi  40144  islptre  40595  fnlimfvre  40650  addccncf2  40833  fsumcncf  40835  cncfperiod  40836  negcncfg  40838  cncfuni  40843  icccncfext  40844  cncficcgt0  40845  fprodcncf  40858  dvcnre  40874  fperdvper  40877  dvmptresicc  40878  itgsinexplem1  40913  itgcoscmulx  40928  submgmid  42592  rnghmsscmap2  42772  rhmsscmap2  42818  fldhmsubc  42883  fldhmsubcALTV  42901  elbigolo1  43150
  Copyright terms: Public domain W3C validator