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

Theorem ollat 35369
 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 35368 . 2 (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
21simplbi 493 1 (𝐾 ∈ OL → 𝐾 ∈ Lat)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2107  Latclat 17431  OPcops 35328  OLcol 35330 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799  df-ol 35334 This theorem is referenced by:  oldmm1  35373  oldmj1  35377  olj01  35381  olj02  35382  olm12  35384  latmassOLD  35385  latm12  35386  latm32  35387  latmrot  35388  latm4  35389  latmmdiN  35390  latmmdir  35391  olm01  35392  olm02  35393  omllat  35398  meetat  35452
 Copyright terms: Public domain W3C validator