Description: Eliminate T. as an antecedent. A proposition implied by T. is true. This is modus ponens ax-mp when the minor hypothesis is T. (which holds by tru ). (Contributed by Mario Carneiro, 13-Mar-2014)