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 39662
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 39660 . 2 (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
21simprbi 497 1 (𝐾 ∈ OL → 𝐾 ∈ OP)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  Latclat 18399  OPcops 39620  OLcol 39622
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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-ol 39626
This theorem is referenced by:  olposN  39663  oldmm1  39665  oldmm2  39666  oldmm3N  39667  oldmm4  39668  oldmj1  39669  oldmj2  39670  oldmj3  39671  oldmj4  39672  olj01  39673  olj02  39674  olm11  39675  olm12  39676  latmassOLD  39677  olm01  39684  olm02  39685  omlop  39689  meetat  39744  hlop  39810  polatN  40379
  Copyright terms: Public domain W3C validator