Theorem hllatd

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

	Ref	Expression
Hypothesis	hllatd.1	|- ( ph -> K e. HL )
Assertion	hllatd	|- ( ph -> K e. Lat )

Proof

Step	Hyp	Ref	Expression
1		hllatd.1	|- ( ph -> K e. HL )
2		hllat	|- ( K e. HL -> K e. Lat )
3	1 2	syl	|- ( ph -> K e. Lat )