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 ] T.

Proof

Step	Hyp	Ref	Expression
1		tru	|- T.
2	1	sbt	|- [ y / x ] T.