Although systems with intersection types have many unique capabilities, there has never been a fully satisfactory explicitly typed system with intersection types. We introduce λ^B with branching types and types which are quantified over type selectors to provide an explicitly typed system with the same expressiveness as a system with intersection types. Typing derivations in λ^B effiectively squash together what would be separate parallel derivations in earlier systems with intersection types.