Metamath Proof Explorer


Theorem muldvds2d

Description: If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses muldvds2d.1 φ K
muldvds2d.2 φ M
muldvds2d.3 φ N
muldvds2d.4 φ K M N
Assertion muldvds2d φ M N

Proof

Step Hyp Ref Expression
1 muldvds2d.1 φ K
2 muldvds2d.2 φ M
3 muldvds2d.3 φ N
4 muldvds2d.4 φ K M N
5 1 2 3 3jca φ K M N
6 muldvds2 K M N K M N M N
7 5 4 6 sylc φ M N