Theorem dvds2addd

Description: Deduction form of dvds2add . (Contributed by SN, 21-Aug-2024)

	Ref	Expression
Hypotheses	dvds2addd.k	$$⊢\phi \to K\in \mathbb{Z}$$
	dvds2addd.m	$$⊢\phi \to M\in \mathbb{Z}$$
	dvds2addd.n	$$⊢\phi \to N\in \mathbb{Z}$$
	dvds2addd.1	$$⊢\phi \to K\parallel M$$
	dvds2addd.2	$$⊢\phi \to K\parallel N$$
Assertion	dvds2addd	$$⊢\phi \to K\parallel \left(M+N\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvds2addd.k	$$⊢\phi \to K\in \mathbb{Z}$$
2		dvds2addd.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		dvds2addd.n	$$⊢\phi \to N\in \mathbb{Z}$$
4		dvds2addd.1	$$⊢\phi \to K\parallel M$$
5		dvds2addd.2	$$⊢\phi \to K\parallel N$$
6		dvds2add	$$⊢\left(K\in \mathbb{Z}\wedge M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(\left(K\parallel M\wedge K\parallel N\right)\to K\parallel \left(M+N\right)\right)$$
7	1 2 3 6	syl3anc	$$⊢\phi \to \left(\left(K\parallel M\wedge K\parallel N\right)\to K\parallel \left(M+N\right)\right)$$
8	4 5 7	mp2and	$$⊢\phi \to K\parallel \left(M+N\right)$$