Theorem ssidd 3204

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  isum  11550  fsum3ser  11562  fsumcl  11565  iprodap  11745  iprodap0  11747  fprodssdc  11755  fprodcl  11772  fprodclf  11800  ennnfoneleminc  12628  submid  13109  mulgnncl  13267  mulgnn0cl  13268  mulgcl  13269  subgid  13305  ablressid  13465  gsumfzreidx  13467  rngressid  13510  ringressid  13619  mulgass3  13641  subrngid  13757  lss1  13918  rlmfn  14009  rlmvalg  14010  rlmbasg  14011  rlmplusgg  14012  rlm0g  14013  rlmmulrg  14015  rlmscabas  14016  rlmvscag  14017  rlmtopng  14018  rlmdsg  14019  restopn2  14419  negcncf  14841  mulcncf  14844  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvexp  14947  dvrecap  14949  dvmptcmulcn  14957  dvmptnegcn  14958  dvmptsubcn  14959  dveflem  14962  dvef  14963  bj-charfundcALT  15455