5.8ex I

The following are applications of SD+'s rules of replacement. They can be nicely completed using just IM, DM, AS, DN, CM and a few rules of inference. (Go ahead and use the "/" shortcut even for the SD+ rules of inference: MT,DS,HS.)