Metamath Proof Explorer


Theorem muldvds1d

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 muldvds1d.1 φ K
muldvds1d.2 φ M
muldvds1d.3 φ N
muldvds1d.4 φ K M N
Assertion muldvds1d φ K N

Proof

Step Hyp Ref Expression
1 muldvds1d.1 φ K
2 muldvds1d.2 φ M
3 muldvds1d.3 φ N
4 muldvds1d.4 φ K M N
5 1 2 3 3jca φ K M N
6 muldvds1 K M N K M N K N
7 5 6 syl φ K M N K N
8 4 7 mpd φ K N