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  11638  fsum3ser  11650  fsumcl  11653  iprodap  11833  iprodap0  11835  fprodssdc  11843  fprodcl  11860  fprodclf  11888  ennnfoneleminc  12724  submid  13251  mulgnncl  13415  mulgnn0cl  13416  mulgcl  13417  subgid  13453  ablressid  13613  gsumfzreidx  13615  rngressid  13658  ringressid  13767  mulgass3  13789  subrngid  13905  lss1  14066  rlmfn  14157  rlmvalg  14158  rlmbasg  14159  rlmplusgg  14160  rlm0g  14161  rlmmulrg  14163  rlmscabas  14164  rlmvscag  14165  rlmtopng  14166  rlmdsg  14167  restopn2  14597  negcncf  15019  mulcncf  15022  dvidlemap  15105  dvidrelem  15106  dvidsslem  15107  dvaddxxbr  15115  dvmulxxbr  15116  dvcoapbr  15121  dvcjbr  15122  dvexp  15125  dvrecap  15127  dvmptcmulcn  15135  dvmptnegcn  15136  dvmptsubcn  15137  dveflem  15140  dvef  15141  bj-charfundcALT  15678