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 39648
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 39646 . 2 (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
21simprbi 497 1 (𝐾 ∈ OL → 𝐾 ∈ OP)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  Latclat 18386  OPcops 39606  OLcol 39608
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 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3429  df-in 3892  df-ol 39612
This theorem is referenced by:  olposN  39649  oldmm1  39651  oldmm2  39652  oldmm3N  39653  oldmm4  39654  oldmj1  39655  oldmj2  39656  oldmj3  39657  oldmj4  39658  olj01  39659  olj02  39660  olm11  39661  olm12  39662  latmassOLD  39663  olm01  39670  olm02  39671  omlop  39675  meetat  39730  hlop  39796  polatN  40365
  Copyright terms: Public domain W3C validator