Theorem ssidd 3245

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  swrd0g  11187  isum  11891  fsum3ser  11903  fsumcl  11906  iprodap  12086  iprodap0  12088  fprodssdc  12096  fprodcl  12113  fprodclf  12141  ennnfoneleminc  12977  submid  13505  mulgnncl  13669  mulgnn0cl  13670  mulgcl  13671  subgid  13707  ablressid  13867  gsumfzreidx  13869  rngressid  13912  ringressid  14021  mulgass3  14043  subrngid  14159  lss1  14320  rlmfn  14411  rlmvalg  14412  rlmbasg  14413  rlmplusgg  14414  rlm0g  14415  rlmmulrg  14417  rlmscabas  14418  rlmvscag  14419  rlmtopng  14420  rlmdsg  14421  restopn2  14851  negcncf  15273  mulcncf  15276  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvcjbr  15376  dvexp  15379  dvrecap  15381  dvmptcmulcn  15389  dvmptnegcn  15390  dvmptsubcn  15391  dveflem  15394  dvef  15395  ifpsnprss  16040  bj-charfundcALT  16130