Description: Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | paddssw.a | ||
paddssw.p | |||
Assertion | paddssw1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | paddssw.a | ||
2 | paddssw.p | ||
3 | simpl | ||
4 | simpr3 | ||
5 | 1 2 | paddss12 | |
6 | 3 4 4 5 | syl3anc |