Theorem hllatd

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

	Ref	Expression
Hypothesis	hllatd.1	$$⊢\phi \to K\in \mathrm{HL}$$
Assertion	hllatd	$$⊢\phi \to K\in \mathrm{Lat}$$

Proof

Step	Hyp	Ref	Expression
1		hllatd.1	$$⊢\phi \to K\in \mathrm{HL}$$
2		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
3	1 2	syl	$$⊢\phi \to K\in \mathrm{Lat}$$