Description: Virtual deduction generalizing rule for one quantifying variables and
two virtual hypothesis. gen21 is alrimdv with virtual deductions.
(Contributed by Alan Sare, 25-Jul-2011)(Proof modification is discouraged.)(New usage is discouraged.)