Theorem parteq12

Description: Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024)

	Ref	Expression
Assertion	parteq12	$$⊢\left(R=S\wedge A=B\right)\to \left(RPartA\leftrightarrow SPartB\right)$$

Proof

Step	Hyp	Ref	Expression
1		parteq1	$$⊢R=S\to \left(RPartA\leftrightarrow SPartA\right)$$
2		parteq2	$$⊢A=B\to \left(SPartA\leftrightarrow SPartB\right)$$
3	1 2	sylan9bb	$$⊢\left(R=S\wedge A=B\right)\to \left(RPartA\leftrightarrow SPartB\right)$$