Theorem hllatd

Description: Deduction form of hllat . A Hilbert lattice is a lattice. (Contributed by BJ, 14-Aug-2022)

	Ref	Expression
Hypothesis	hllatd.1	⊢ ( 𝜑 → 𝐾 ∈ HL )
Assertion	hllatd	⊢ ( 𝜑 → 𝐾 ∈ Lat )

Proof

Step	Hyp	Ref	Expression
1		hllatd.1	⊢ ( 𝜑 → 𝐾 ∈ HL )
2		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
3	1 2	syl	⊢ ( 𝜑 → 𝐾 ∈ Lat )