Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ollat Structured version   Visualization version   GIF version

Theorem ollat 36409
 Description: An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
ollat (𝐾 ∈ OL → 𝐾 ∈ Lat)

Proof of Theorem ollat
StepHypRef Expression
1 isolat 36408 . 2 (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
21simplbi 501 1 (𝐾 ∈ OL → 𝐾 ∈ Lat)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2115  Latclat 17644  OPcops 36368  OLcol 36370 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3481  df-in 3925  df-ol 36374 This theorem is referenced by:  oldmm1  36413  oldmj1  36417  olj01  36421  olj02  36422  olm12  36424  latmassOLD  36425  latm12  36426  latm32  36427  latmrot  36428  latm4  36429  latmmdiN  36430  latmmdir  36431  olm01  36432  olm02  36433  omllat  36438  meetat  36492
 Copyright terms: Public domain W3C validator