Metamath Proof Explorer


Theorem mptru

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)

Ref Expression
Hypothesis mptru.1
|- ( T. -> ph )
Assertion mptru
|- ph

Proof

Step Hyp Ref Expression
1 mptru.1
 |-  ( T. -> ph )
2 tru
 |-  T.
3 2 1 ax-mp
 |-  ph