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

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 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
dvdstrd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
dvdstrd.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
dvdstrd.4 ⊢ ( 𝜑 → 𝐾 ∥ 𝑀 )
dvdstrd.5 ⊢ ( 𝜑 → 𝑀 ∥ 𝑁 )
Assertion dvdstrd ( 𝜑 → 𝐾 ∥ 𝑁 )

Proof

Step Hyp Ref Expression
1 dvdstrd.1 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2 dvdstrd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 dvdstrd.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 dvdstrd.4 ⊢ ( 𝜑 → 𝐾 ∥ 𝑀 )
5 dvdstrd.5 ⊢ ( 𝜑 → 𝑀 ∥ 𝑁 )
6 dvdstr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝑀 ∥ 𝑁 ) → 𝐾 ∥ 𝑁 ) )
7 1 2 3 6 syl3anc ⊢ ( 𝜑 → ( ( 𝐾 ∥ 𝑀 ∧ 𝑀 ∥ 𝑁 ) → 𝐾 ∥ 𝑁 ) )
8 4 5 7 mp2and ⊢ ( 𝜑 → 𝐾 ∥ 𝑁 )