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

Metamath Proof Explorer

Theorem nftru

Description: The true constant has no free variables. (This can also be proven in one step with nfv , but this proof does not use ax-5 .) (Contributed by Mario Carneiro, 6-Oct-2016)

		Ref	Expression
	Assertion	nftru	⊢ Ⅎ 𝑥 ⊤

Proof

Step	Hyp	Ref	Expression
1		tru	⊢ ⊤
2	1	nfth	⊢ Ⅎ 𝑥 ⊤