Theorem ssidd 3269

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  suppofss1dcl  6494  suppofss2dcl  6495  swrd0g  11410  isum  12130  fsum3ser  12142  fsumcl  12145  iprodap  12325  iprodap0  12327  fprodssdc  12335  fprodcl  12352  fprodclf  12380  ennnfoneleminc  13280  submid  13761  mulgnncl  13917  mulgnn0cl  13918  mulgcl  13919  subgid  13955  ablressid  14116  gzsumreidx  14118  gsumvalfi  14129  gsummptfidmadd  14138  rngressid  14228  ringressid  14341  mulgass3  14364  subrngid  14482  lss1  14671  rlmfn  14762  rlmvalg  14763  rlmbasg  14764  rlmplusgg  14765  rlm0g  14766  rlmmulrg  14768  rlmscabas  14769  rlmvscag  14770  rlmtopng  14771  rlmdsg  14772  restopn2  15207  negcncf  15629  mulcncf  15632  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvexp  15735  dvrecap  15737  dvmptcmulcn  15745  dvmptnegcn  15746  dvmptsubcn  15747  dveflem  15750  dvef  15751  ifpsnprss  16498  bj-charfundcALT  16749