Theorem ollat 40377

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Latclat 18612  OPcops 40336  OLcol 40338

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090  df-ol 40342

This theorem is used by:  oldmm1  40381  oldmj1  40385  olj01  40389  olj02  40390  olm12  40392  latmassOLD  40393  latm12  40394  latm32  40395  latmrot  40396  latm4  40397  latmmdiN  40398  latmmdir  40399  olm01  40400  olm02  40401  omllat  40406  meetat  40460