Theorem ssidd 3249

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  suppofss1dcl  6442  suppofss2dcl  6443  swrd0g  11290  isum  12009  fsum3ser  12021  fsumcl  12024  iprodap  12204  iprodap0  12206  fprodssdc  12214  fprodcl  12231  fprodclf  12259  ennnfoneleminc  13095  submid  13623  mulgnncl  13787  mulgnn0cl  13788  mulgcl  13789  subgid  13825  ablressid  13985  gsumfzreidx  13987  rngressid  14031  ringressid  14140  mulgass3  14162  subrngid  14279  lss1  14441  rlmfn  14532  rlmvalg  14533  rlmbasg  14534  rlmplusgg  14535  rlm0g  14536  rlmmulrg  14538  rlmscabas  14539  rlmvscag  14540  rlmtopng  14541  rlmdsg  14542  restopn2  14977  negcncf  15399  mulcncf  15402  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcjbr  15502  dvexp  15505  dvrecap  15507  dvmptcmulcn  15515  dvmptnegcn  15516  dvmptsubcn  15517  dveflem  15520  dvef  15521  ifpsnprss  16267  bj-charfundcALT  16508  gfsumval  16792