Metamath Proof Explorer

Theorem suceqd

Description: Deduction associated with suceq . (Contributed by Rohan Ridenour, 8-Aug-2023)

Ref Expression
Hypothesis suceqd.1 
|- ( ph -> A = B )
Assertion suceqd 
|- ( ph -> suc A = suc B )

Proof

Step Hyp Ref Expression
1 suceqd.1 
 |-  ( ph -> A = B )
2 suceq 
 |-  ( A = B -> suc A = suc B )
3 1 2 syl 
 |-  ( ph -> suc A = suc B )