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  11192  isum  11896  fsum3ser  11908  fsumcl  11911  iprodap  12091  iprodap0  12093  fprodssdc  12101  fprodcl  12118  fprodclf  12146  ennnfoneleminc  12982  submid  13510  mulgnncl  13674  mulgnn0cl  13675  mulgcl  13676  subgid  13712  ablressid  13872  gsumfzreidx  13874  rngressid  13917  ringressid  14026  mulgass3  14048  subrngid  14165  lss1  14326  rlmfn  14417  rlmvalg  14418  rlmbasg  14419  rlmplusgg  14420  rlm0g  14421  rlmmulrg  14423  rlmscabas  14424  rlmvscag  14425  rlmtopng  14426  rlmdsg  14427  restopn2  14857  negcncf  15279  mulcncf  15282  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvaddxxbr  15375  dvmulxxbr  15376  dvcoapbr  15381  dvcjbr  15382  dvexp  15385  dvrecap  15387  dvmptcmulcn  15395  dvmptnegcn  15396  dvmptsubcn  15397  dveflem  15400  dvef  15401  ifpsnprss  16054  bj-charfundcALT  16172