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  11432  isum  12152  fsum3ser  12164  fsumcl  12167  iprodap  12347  iprodap0  12349  fprodssdc  12357  fprodcl  12374  fprodclf  12402  ennnfoneleminc  13302  submid  13784  mulgnncl  13940  mulgnn0cl  13941  mulgcl  13942  subgid  13978  ablressid  14139  gzsumreidx  14141  gsumvalfi  14152  gsummptfidmadd  14161  rngressid  14253  ringressid  14368  mulgass3  14391  subrngid  14509  lss1  14699  rlmfn  14790  rlmvalg  14791  rlmbasg  14792  rlmplusgg  14793  rlm0g  14794  rlmmulrg  14796  rlmscabas  14797  rlmvscag  14798  rlmtopng  14799  rlmdsg  14800  rnasclassa  15038  restopn2  15284  negcncf  15706  mulcncf  15709  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvexp  15812  dvrecap  15814  dvmptcmulcn  15822  dvmptnegcn  15823  dvmptsubcn  15824  dveflem  15827  dvef  15828  ifpsnprss  16584  bj-charfundcALT  16835