Description: Inference associated with ifcl . Membership (closure) of a
conditional operator. Also usable to keep a membership hypothesis for
the weak deduction theorem dedth when the special case B e. C is
provable. (Contributed by NM, 14-Aug-1999)(Proof shortened by BJ, 1-Sep-2022)