Theorem ssidd 3269

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

Assertion

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

Proof of Theorem ssidd

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

This proof depends on syntax axioms:   -> wi 4   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  suppofss1dcl  6504  suppofss2dcl  6505  swrd0g  11446  isum  12168  fsum3ser  12180  fsumcl  12183  iprodap  12363  iprodap0  12365  fprodssdc  12373  fprodcl  12390  fprodclf  12418  ennnfoneleminc  13351  submid  13833  mulgnncl  13989  mulgnn0cl  13990  mulgcl  13991  subgid  14027  ablressid  14188  gzsumreidx  14190  gsumvalfi  14201  gsummptfidmadd  14210  rngressid  14302  ringressid  14417  mulgass3  14440  subrngid  14558  lss1  14748  rlmfn  14839  rlmvalg  14840  rlmbasg  14841  rlmplusgg  14842  rlm0g  14843  rlmmulrg  14845  rlmscabas  14846  rlmvscag  14847  rlmtopng  14848  rlmdsg  14849  rnasclassa  15087  restopn2  15333  negcncf  15755  mulcncf  15758  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvexp  15861  dvrecap  15863  dvmptcmulcn  15871  dvmptnegcn  15872  dvmptsubcn  15873  dveflem  15876  dvef  15877  ifpsnprss  16682  bj-charfundcALT  16933