Users' Mathboxes 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