This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvds2addd

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

Ref Expression
Hypotheses dvds2addd.k ⊢ φ → K ∈ ℤ
dvds2addd.m ⊢ φ → M ∈ ℤ
dvds2addd.n ⊢ φ → N ∈ ℤ
dvds2addd.1 ⊢ φ → K ∥ M
dvds2addd.2 ⊢ φ → K ∥ N
Assertion dvds2addd ⊢ φ → K ∥ M + N

Proof

Step Hyp Ref Expression
1 dvds2addd.k ⊢ φ → K ∈ ℤ
2 dvds2addd.m ⊢ φ → M ∈ ℤ
3 dvds2addd.n ⊢ φ → N ∈ ℤ
4 dvds2addd.1 ⊢ φ → K ∥ M
5 dvds2addd.2 ⊢ φ → K ∥ N
6 dvds2add ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∥ M ∧ K ∥ N → K ∥ M + N
7 1 2 3 6 syl3anc ⊢ φ → K ∥ M ∧ K ∥ N → K ∥ M + N
8 4 5 7 mp2and ⊢ φ → K ∥ M + N