This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ ⊤ \to φ$
	Assertion	mptru	$⊢ φ$

Proof

Step	Hyp	Ref	Expression
1		mptru.1	$⊢ ⊤ \to φ$
2		tru	$⊢ ⊤$
3	2 1	ax-mp	$⊢ φ$