Theorem ollat 40020

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 40019	. 2 ⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
2	1	simplbi 502	1 ⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Latclat 18505  OPcops 39979  OLcol 39981

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-ol 39985

This theorem is used by:  oldmm1  40024  oldmj1  40028  olj01  40032  olj02  40033  olm12  40035  latmassOLD  40036  latm12  40037  latm32  40038  latmrot  40039  latm4  40040  latmmdiN  40041  latmmdir  40042  olm01  40043  olm02  40044  omllat  40049  meetat  40103