Metamath Proof Explorer

Theorem sbtru

Description: The result of substituting in the truth constant "true" is true. (Contributed by BJ, 2-Sep-2023)

		Ref	Expression
	Assertion	sbtru	$⊢ [y/ x] ⊤$

Step	Hyp	Ref	Expression
1		tru	$⊢ ⊤$
2	1	sbt	$⊢ [y/ x] ⊤$