Theorem ssidd 3201

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  isum  11531  fsum3ser  11543  fsumcl  11546  iprodap  11726  iprodap0  11728  fprodssdc  11736  fprodcl  11753  fprodclf  11781  ennnfoneleminc  12571  submid  13052  mulgnncl  13210  mulgnn0cl  13211  mulgcl  13212  subgid  13248  ablressid  13408  gsumfzreidx  13410  rngressid  13453  ringressid  13562  mulgass3  13584  subrngid  13700  lss1  13861  rlmfn  13952  rlmvalg  13953  rlmbasg  13954  rlmplusgg  13955  rlm0g  13956  rlmmulrg  13958  rlmscabas  13959  rlmvscag  13960  rlmtopng  13961  rlmdsg  13962  restopn2  14362  negcncf  14784  mulcncf  14787  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvexp  14890  dvrecap  14892  dvmptcmulcn  14900  dvmptnegcn  14901  dvmptsubcn  14902  dveflem  14905  dvef  14906  bj-charfundcALT  15371