Metamath Proof Explorer


Theorem suceqd

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

Ref Expression
Hypothesis suceqd.1 ( 𝜑𝐴 = 𝐵 )
Assertion suceqd ( 𝜑 → suc 𝐴 = suc 𝐵 )

Proof

Step Hyp Ref Expression
1 suceqd.1 ( 𝜑𝐴 = 𝐵 )
2 suceq ( 𝐴 = 𝐵 → suc 𝐴 = suc 𝐵 )
3 1 2 syl ( 𝜑 → suc 𝐴 = suc 𝐵 )