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 φKM
dvds2addd.2 φKN
Assertion dvds2addd φKM+N

Proof

Step Hyp Ref Expression
1 dvds2addd.k φK
2 dvds2addd.m φM
3 dvds2addd.n φN
4 dvds2addd.1 φKM
5 dvds2addd.2 φKN
6 dvds2add KMNKMKNKM+N
7 1 2 3 6 syl3anc φKMKNKM+N
8 4 5 7 mp2and φKM+N