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