Theorem ssidd 3248

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  swrd0g  11240  isum  11945  fsum3ser  11957  fsumcl  11960  iprodap  12140  iprodap0  12142  fprodssdc  12150  fprodcl  12167  fprodclf  12195  ennnfoneleminc  13031  submid  13559  mulgnncl  13723  mulgnn0cl  13724  mulgcl  13725  subgid  13761  ablressid  13921  gsumfzreidx  13923  rngressid  13966  ringressid  14075  mulgass3  14097  subrngid  14214  lss1  14375  rlmfn  14466  rlmvalg  14467  rlmbasg  14468  rlmplusgg  14469  rlm0g  14470  rlmmulrg  14472  rlmscabas  14473  rlmvscag  14474  rlmtopng  14475  rlmdsg  14476  restopn2  14906  negcncf  15328  mulcncf  15331  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  dvexp  15434  dvrecap  15436  dvmptcmulcn  15444  dvmptnegcn  15445  dvmptsubcn  15446  dveflem  15449  dvef  15450  ifpsnprss  16193  bj-charfundcALT  16404  gfsumval  16680