Theorem ssidd 3200

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3153

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 3159  df-ss 3166

This theorem is referenced by:  isum  11528  fsum3ser  11540  fsumcl  11543  iprodap  11723  iprodap0  11725  fprodssdc  11733  fprodcl  11750  fprodclf  11778  ennnfoneleminc  12568  submid  13049  mulgnncl  13207  mulgnn0cl  13208  mulgcl  13209  subgid  13245  ablressid  13405  gsumfzreidx  13407  rngressid  13450  ringressid  13559  mulgass3  13581  subrngid  13697  lss1  13858  rlmfn  13949  rlmvalg  13950  rlmbasg  13951  rlmplusgg  13952  rlm0g  13953  rlmmulrg  13955  rlmscabas  13956  rlmvscag  13957  rlmtopng  13958  rlmdsg  13959  restopn2  14351  negcncf  14759  mulcncf  14762  dvidlemap  14845  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvexp  14860  dvrecap  14862  dvmptcmulcn  14868  dvmptnegcn  14869  dvmptsubcn  14870  dveflem  14872  dvef  14873  bj-charfundcALT  15301