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

Metamath Proof Explorer

Theorem omllat

Description: An orthomodular lattice is a lattice. (Contributed by NM, 6-Nov-2011)

Ref Expression
Assertion omllat ( 𝐾 ∈ OML → 𝐾 ∈ Lat )

Proof

Step Hyp Ref Expression
1 omlol ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OL )
2 ollat ⊢ ( 𝐾 ∈ OL → 𝐾 ∈ Lat )
3 1 2 syl ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )