Theorem ssidd 3263

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

Assertion

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

Proof of Theorem ssidd

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

Syntax hints:   -> wi 4   C_ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  suppofss1dcl  6477  suppofss2dcl  6478  swrd0g  11377  isum  12096  fsum3ser  12108  fsumcl  12111  iprodap  12291  iprodap0  12293  fprodssdc  12301  fprodcl  12318  fprodclf  12346  ennnfoneleminc  13246  submid  13732  mulgnncl  13890  mulgnn0cl  13891  mulgcl  13892  subgid  13928  ablressid  14088  gsumfzreidx  14090  gfsumval  14102  rngressid  14193  ringressid  14306  mulgass3  14329  subrngid  14447  lss1  14636  rlmfn  14727  rlmvalg  14728  rlmbasg  14729  rlmplusgg  14730  rlm0g  14731  rlmmulrg  14733  rlmscabas  14734  rlmvscag  14735  rlmtopng  14736  rlmdsg  14737  restopn2  15174  negcncf  15596  mulcncf  15599  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvexp  15702  dvrecap  15704  dvmptcmulcn  15712  dvmptnegcn  15713  dvmptsubcn  15714  dveflem  15717  dvef  15718  ifpsnprss  16464  bj-charfundcALT  16705