Theorem ssidd 3259

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  suppofss1dcl  6464  suppofss2dcl  6465  swrd0g  11352  isum  12071  fsum3ser  12083  fsumcl  12086  iprodap  12266  iprodap0  12268  fprodssdc  12276  fprodcl  12293  fprodclf  12321  ennnfoneleminc  13162  submid  13690  mulgnncl  13854  mulgnn0cl  13855  mulgcl  13856  subgid  13892  ablressid  14052  gsumfzreidx  14054  rngressid  14098  ringressid  14207  mulgass3  14229  subrngid  14346  lss1  14510  rlmfn  14601  rlmvalg  14602  rlmbasg  14603  rlmplusgg  14604  rlm0g  14605  rlmmulrg  14607  rlmscabas  14608  rlmvscag  14609  rlmtopng  14610  rlmdsg  14611  restopn2  15048  negcncf  15470  mulcncf  15473  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  dvexp  15576  dvrecap  15578  dvmptcmulcn  15586  dvmptnegcn  15587  dvmptsubcn  15588  dveflem  15591  dvef  15592  ifpsnprss  16338  bj-charfundcALT  16579  gfsumval  16862