Theorem sbtru

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

	Ref	Expression
Assertion	sbtru	⊢ [ 𝑦 / 𝑥 ] ⊤

Proof

Step	Hyp	Ref	Expression
1		tru	⊢ ⊤
2	1	sbt	⊢ [ 𝑦 / 𝑥 ] ⊤