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  6497  suppofss2dcl  6498  swrd0g  11413  isum  12133  fsum3ser  12145  fsumcl  12148  iprodap  12328  iprodap0  12330  fprodssdc  12338  fprodcl  12355  fprodclf  12383  ennnfoneleminc  13283  submid  13764  mulgnncl  13920  mulgnn0cl  13921  mulgcl  13922  subgid  13958  ablressid  14119  gzsumreidx  14121  gsumvalfi  14132  gsummptfidmadd  14141  rngressid  14231  ringressid  14344  mulgass3  14367  subrngid  14485  lss1  14674  rlmfn  14765  rlmvalg  14766  rlmbasg  14767  rlmplusgg  14768  rlm0g  14769  rlmmulrg  14771  rlmscabas  14772  rlmvscag  14773  rlmtopng  14774  rlmdsg  14775  restopn2  15210  negcncf  15632  mulcncf  15635  dvidlemap  15718  dvidrelem  15719  dvidsslem  15720  dvaddxxbr  15728  dvmulxxbr  15729  dvcoapbr  15734  dvcjbr  15735  dvexp  15738  dvrecap  15740  dvmptcmulcn  15748  dvmptnegcn  15749  dvmptsubcn  15750  dveflem  15753  dvef  15754  ifpsnprss  16501  bj-charfundcALT  16752