Theorem ollat 36509

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

Syntax hints:   → wi 4   ∈ wcel 2111  Latclat 17647  OPcops 36468  OLcol 36470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ol 36474

This theorem is referenced by:  oldmm1  36513  oldmj1  36517  olj01  36521  olj02  36522  olm12  36524  latmassOLD  36525  latm12  36526  latm32  36527  latmrot  36528  latm4  36529  latmmdiN  36530  latmmdir  36531  olm01  36532  olm02  36533  omllat  36538  meetat  36592