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  11448  isum  12171  fsum3ser  12183  fsumcl  12186  iprodap  12366  iprodap0  12368  fprodssdc  12376  fprodcl  12393  fprodclf  12421  ennnfoneleminc  13354  submid  13837  mulgnncl  13993  mulgnn0cl  13994  mulgcl  13995  subgid  14031  ablressid  14223  gzsumreidx  14225  gsumvalfi  14236  gsummptfidmadd  14245  rngressid  14337  ringressid  14452  mulgass3  14475  subrngid  14593  lss1  14783  rlmfn  14874  rlmvalg  14875  rlmbasg  14876  rlmplusgg  14877  rlm0g  14878  rlmmulrg  14880  rlmscabas  14881  rlmvscag  14882  rlmtopng  14883  rlmdsg  14884  rnasclassa  15122  restopn2  15375  negcncf  15797  mulcncf  15800  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvexp  15903  dvrecap  15905  dvmptcmulcn  15913  dvmptnegcn  15914  dvmptsubcn  15915  dveflem  15918  dvef  15919  ifpsnprss  16750  bj-charfundcALT  17001