Theorem ssidd 3246

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  swrd0g  11231  isum  11936  fsum3ser  11948  fsumcl  11951  iprodap  12131  iprodap0  12133  fprodssdc  12141  fprodcl  12158  fprodclf  12186  ennnfoneleminc  13022  submid  13550  mulgnncl  13714  mulgnn0cl  13715  mulgcl  13716  subgid  13752  ablressid  13912  gsumfzreidx  13914  rngressid  13957  ringressid  14066  mulgass3  14088  subrngid  14205  lss1  14366  rlmfn  14457  rlmvalg  14458  rlmbasg  14459  rlmplusgg  14460  rlm0g  14461  rlmmulrg  14463  rlmscabas  14464  rlmvscag  14465  rlmtopng  14466  rlmdsg  14467  restopn2  14897  negcncf  15319  mulcncf  15322  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  dvexp  15425  dvrecap  15427  dvmptcmulcn  15435  dvmptnegcn  15436  dvmptsubcn  15437  dveflem  15440  dvef  15441  ifpsnprss  16140  bj-charfundcALT  16340