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

Metamath Proof Explorer

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 )