Description: Virtual deduction rule e120 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)