Theorem ollat 40250

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Latclat 18598  OPcops 40209  OLcol 40211

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ol 40215

This theorem is used by:  oldmm1  40254  oldmj1  40258  olj01  40262  olj02  40263  olm12  40265  latmassOLD  40266  latm12  40267  latm32  40268  latmrot  40269  latm4  40270  latmmdiN  40271  latmmdir  40272  olm01  40273  olm02  40274  omllat  40279  meetat  40333