Theorem suceqd

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

	Ref	Expression
Hypothesis	suceqd.1	$$⊢\phi \to A=B$$
Assertion	suceqd	$$⊢\phi \to \mathrm{suc}A=\mathrm{suc}B$$

Proof

Step	Hyp	Ref	Expression
1		suceqd.1	$$⊢\phi \to A=B$$
2		suceq	$$⊢A=B\to \mathrm{suc}A=\mathrm{suc}B$$
3	1 2	syl	$$⊢\phi \to \mathrm{suc}A=\mathrm{suc}B$$