Description: Weak deduction theorem that eliminates a hypothesis ph , making it
become an antecedent. We assume that a proof exists for ph when the
class variable A is replaced with a specific class B . The
hypothesis ch should be assigned to the inference, and the inference
hypothesis eliminated with elimhyp . If the inference has other
hypotheses with class variable A , these can be kept by assigning
keephyp to them. For more information, see the Weak Deduction Theorem
page mmdeduction.html . (Contributed by NM, 15-May-1999)