Metamath Proof Explorer


Theorem dvdstrd

Description: The divides relation is transitive, a deduction version of dvdstr . (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses dvdstrd.1 φK
dvdstrd.2 φM
dvdstrd.3 φN
dvdstrd.4 φKM
dvdstrd.5 φMN
Assertion dvdstrd φKN

Proof

Step Hyp Ref Expression
1 dvdstrd.1 φK
2 dvdstrd.2 φM
3 dvdstrd.3 φN
4 dvdstrd.4 φKM
5 dvdstrd.5 φMN
6 dvdstr KMNKMMNKN
7 1 2 3 6 syl3anc φKMMNKN
8 4 5 7 mp2and φKN