Theorem ollat 39211

Description: An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.)

Assertion

Ref	Expression
ollat	⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat)

Proof of Theorem ollat

Step	Hyp	Ref	Expression
1		isolat 39210	. 2 ⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
2	1	simplbi 497	1 ⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat)

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18356  OPcops 39170  OLcol 39172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-in 3912  df-ol 39176

This theorem is referenced by:  oldmm1  39215  oldmj1  39219  olj01  39223  olj02  39224  olm12  39226  latmassOLD  39227  latm12  39228  latm32  39229  latmrot  39230  latm4  39231  latmmdiN  39232  latmmdir  39233  olm01  39234  olm02  39235  omllat  39240  meetat  39294