Theorem ollat 40086

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Latclat 18519  OPcops 40045  OLcol 40047

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-ol 40051

This theorem is used by:  oldmm1  40090  oldmj1  40094  olj01  40098  olj02  40099  olm12  40101  latmassOLD  40102  latm12  40103  latm32  40104  latmrot  40105  latm4  40106  latmmdiN  40107  latmmdir  40108  olm01  40109  olm02  40110  omllat  40115  meetat  40169