Description: A virtual deduction with 1 virtual hypothesis virtually inferring a
virtual conclusion infers that the same conclusion is virtually inferred
by the same virtual hypothesis and an additional hypothesis.
(Contributed by Alan Sare, 12-Jun-2011)(Proof modification is discouraged.)(New usage is discouraged.)