Rule conjI to split all the terms

Question

The rule conjI splits a conjunction as follows:

show "A ^ B ^ C ^ D"
proof(rule conjI)
  show "A" sorry
next 
  show "C ^ D" sorry"

Is there any rule that splits all the terms connected by the conjunction? Some like:

show "A ^ B ^ C ^ D"
proof(rule ?)
  show "A" sorry
next 
  show "C" sorry"
next 
  show "D" sorry"

Answer 1

You can't do that with a single rule application, but you can do intro conjI to apply it exhaustively.

There's also the method safe that does a variety of things like this (split products, apply appropriate introduction/elimination rules etc).