Description: Version of 3impexp where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011)