5.7ex IV
The following are simple applications of SD+'s rules of replacement. (Go ahead and use the "/" shortcut even for the SD+ rules of inference: MT,DS,HS.)