Theorem ssidd 3213

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  isum  11667  fsum3ser  11679  fsumcl  11682  iprodap  11862  iprodap0  11864  fprodssdc  11872  fprodcl  11889  fprodclf  11917  ennnfoneleminc  12753  submid  13280  mulgnncl  13444  mulgnn0cl  13445  mulgcl  13446  subgid  13482  ablressid  13642  gsumfzreidx  13644  rngressid  13687  ringressid  13796  mulgass3  13818  subrngid  13934  lss1  14095  rlmfn  14186  rlmvalg  14187  rlmbasg  14188  rlmplusgg  14189  rlm0g  14190  rlmmulrg  14192  rlmscabas  14193  rlmvscag  14194  rlmtopng  14195  rlmdsg  14196  restopn2  14626  negcncf  15048  mulcncf  15051  dvidlemap  15134  dvidrelem  15135  dvidsslem  15136  dvaddxxbr  15144  dvmulxxbr  15145  dvcoapbr  15150  dvcjbr  15151  dvexp  15154  dvrecap  15156  dvmptcmulcn  15164  dvmptnegcn  15165  dvmptsubcn  15166  dveflem  15169  dvef  15170  bj-charfundcALT  15707