Theorem ssidd 3248

Description: Weakening of ssid 3247. (Contributed by BJ, 1-Sep-2022.)

Assertion

Ref	Expression
ssidd	|- ( ph -> A C_ A )

Proof of Theorem ssidd

Step	Hyp	Ref	Expression
1		ssid 3247	. 2 |- A C_ A
2	1	a1i 9	1 |- ( ph -> A C_ A )

Syntax hints:   -> wi 4   C_ wss 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  swrd0g  11245  isum  11964  fsum3ser  11976  fsumcl  11979  iprodap  12159  iprodap0  12161  fprodssdc  12169  fprodcl  12186  fprodclf  12214  ennnfoneleminc  13050  submid  13578  mulgnncl  13742  mulgnn0cl  13743  mulgcl  13744  subgid  13780  ablressid  13940  gsumfzreidx  13942  rngressid  13986  ringressid  14095  mulgass3  14117  subrngid  14234  lss1  14395  rlmfn  14486  rlmvalg  14487  rlmbasg  14488  rlmplusgg  14489  rlm0g  14490  rlmmulrg  14492  rlmscabas  14493  rlmvscag  14494  rlmtopng  14495  rlmdsg  14496  restopn2  14926  negcncf  15348  mulcncf  15351  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvcjbr  15451  dvexp  15454  dvrecap  15456  dvmptcmulcn  15464  dvmptnegcn  15465  dvmptsubcn  15466  dveflem  15469  dvef  15470  ifpsnprss  16213  bj-charfundcALT  16455  gfsumval  16732