Description: The virtual deduction introduction rule of converting the end virtual
hypothesis of 2 virtual hypotheses into an antecedent. Conventional
form of int2 is ex . (Contributed by Alan Sare, 23-Apr-2015)(Proof modification is discouraged.)(New usage is discouraged.)