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  6508  suppofss2dcl  6509  swrd0g  11454  isum  12177  fsum3ser  12189  fsumcl  12192  iprodap  12372  iprodap0  12374  fprodssdc  12382  fprodcl  12399  fprodclf  12427  ennnfoneleminc  13360  submid  13843  mulgnncl  13999  mulgnn0cl  14000  mulgcl  14001  subgid  14037  ablressid  14229  gzsumreidx  14231  gsumvalfi  14242  gsummptfidmadd  14251  rngressid  14360  ringressid  14477  mulgass3  14500  subrngid  14618  lss1  14808  rlmfn  14899  rlmvalg  14900  rlmbasg  14901  rlmplusgg  14902  rlm0g  14903  rlmmulrg  14905  rlmscabas  14906  rlmvscag  14907  rlmtopng  14908  rlmdsg  14909  rnasclassa  15147  restopn2  15409  negcncf  15831  mulcncf  15834  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvexp  15937  dvrecap  15939  dvmptcmulcn  15947  dvmptnegcn  15948  dvmptsubcn  15949  dveflem  15952  dvef  15953  ifpsnprss  16789  bj-charfundcALT  17040