Theorem ttceqi

Description: Equality inference for transitive closure. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Hypothesis	ttceqi.1	|- A = B
Assertion	ttceqi	|- TC+ A = TC+ B

Proof

Step	Hyp	Ref	Expression
1		ttceqi.1	|- A = B
2		ttceq	|- ( A = B -> TC+ A = TC+ B )
3	1 2	ax-mp	|- TC+ A = TC+ B