Theorem ssidd 3245

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  swrd0g  11207  isum  11911  fsum3ser  11923  fsumcl  11926  iprodap  12106  iprodap0  12108  fprodssdc  12116  fprodcl  12133  fprodclf  12161  ennnfoneleminc  12997  submid  13525  mulgnncl  13689  mulgnn0cl  13690  mulgcl  13691  subgid  13727  ablressid  13887  gsumfzreidx  13889  rngressid  13932  ringressid  14041  mulgass3  14063  subrngid  14180  lss1  14341  rlmfn  14432  rlmvalg  14433  rlmbasg  14434  rlmplusgg  14435  rlm0g  14436  rlmmulrg  14438  rlmscabas  14439  rlmvscag  14440  rlmtopng  14441  rlmdsg  14442  restopn2  14872  negcncf  15294  mulcncf  15297  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvcjbr  15397  dvexp  15400  dvrecap  15402  dvmptcmulcn  15410  dvmptnegcn  15411  dvmptsubcn  15412  dveflem  15415  dvef  15416  ifpsnprss  16084  bj-charfundcALT  16227