Theorem ollat 39872

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

Syntax hints:   → wi 4   ∈ wcel 2149  Latclat 18483  OPcops 39831  OLcol 39833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-ol 39837

This theorem is referenced by:  oldmm1  39876  oldmj1  39880  olj01  39884  olj02  39885  olm12  39887  latmassOLD  39888  latm12  39889  latm32  39890  latmrot  39891  latm4  39892  latmmdiN  39893  latmmdir  39894  olm01  39895  olm02  39896  omllat  39901  meetat  39955