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

Theorem olop 35289
 Description: An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
olop (𝐾 ∈ OL → 𝐾 ∈ OP)

Proof of Theorem olop
StepHypRef Expression
1 isolat 35287 . 2 (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
21simprbi 492 1 (𝐾 ∈ OL → 𝐾 ∈ OP)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2166  Latclat 17398  OPcops 35247  OLcol 35249 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-ol 35253 This theorem is referenced by:  olposN  35290  oldmm1  35292  oldmm2  35293  oldmm3N  35294  oldmm4  35295  oldmj1  35296  oldmj2  35297  oldmj3  35298  oldmj4  35299  olj01  35300  olj02  35301  olm11  35302  olm12  35303  latmassOLD  35304  olm01  35311  olm02  35312  omlop  35316  meetat  35371  hlop  35437  polatN  36006
 Copyright terms: Public domain W3C validator