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

Metamath Proof Explorer

Theorem dvds2subd

Description: Deduction form of dvds2sub . (Contributed by Stanislas Polu, 9-Mar-2020)

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

Proof

Step Hyp Ref Expression
1 dvds2subd.k ⊢ φ → K ∈ ℤ
2 dvds2subd.m ⊢ φ → M ∈ ℤ
3 dvds2subd.n ⊢ φ → N ∈ ℤ
4 dvds2subd.1 ⊢ φ → K ∥ M
5 dvds2subd.2 ⊢ φ → K ∥ N
6 dvds2sub ⊢ 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