Theorem dvdsexpad

Description: Deduction associated with dvdsexpim . (Contributed by SN, 21-Aug-2024)

	Ref	Expression
Hypotheses	dvdsexpad.1	$$⊢\phi \to A\in \mathbb{Z}$$
	dvdsexpad.2	$$⊢\phi \to B\in \mathbb{Z}$$
	dvdsexpad.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	dvdsexpad.5	$$⊢\phi \to A\parallel B$$
Assertion	dvdsexpad	$$⊢\phi \to A^N\parallel B^N$$

Proof

Step	Hyp	Ref	Expression
1		dvdsexpad.1	$$⊢\phi \to A\in \mathbb{Z}$$
2		dvdsexpad.2	$$⊢\phi \to B\in \mathbb{Z}$$
3		dvdsexpad.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
4		dvdsexpad.5	$$⊢\phi \to A\parallel B$$
5		dvdsexpim	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\wedge N\in {\mathbb{N}}_0\right)\to \left(A\parallel B\to A^N\parallel B^N\right)$$
6	1 2 3 5	syl3anc	$$⊢\phi \to \left(A\parallel B\to A^N\parallel B^N\right)$$
7	4 6	mpd	$$⊢\phi \to A^N\parallel B^N$$