Description: The virtual deduction introduction rule converting the second conjunct
of the second virtual hypothesis into the antecedent of the conclusion.
expd is the non-virtual deduction form of in2an . (Contributed by Alan Sare, 30-Jun-2012)(Proof modification is discouraged.)(New usage is discouraged.)