Metamath Proof Explorer

Theorem ttceqd

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

Ref Expression
Hypothesis ttceqd.1 
|- ( ph -> A = B )
Assertion ttceqd 
|- ( ph -> TC+ A = TC+ B )

Proof

Step Hyp Ref Expression
1 ttceqd.1 
 |-  ( ph -> A = B )
2 ttceq 
 |-  ( A = B -> TC+ A = TC+ B )
3 1 2 syl 
 |-  ( ph -> TC+ A = TC+ B )