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

Theorem olop 36420
 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 36418 . 2 (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
21simprbi 500 1 (𝐾 ∈ OL → 𝐾 ∈ OP)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2115  Latclat 17651  OPcops 36378  OLcol 36380 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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ol 36384 This theorem is referenced by:  olposN  36421  oldmm1  36423  oldmm2  36424  oldmm3N  36425  oldmm4  36426  oldmj1  36427  oldmj2  36428  oldmj3  36429  oldmj4  36430  olj01  36431  olj02  36432  olm11  36433  olm12  36434  latmassOLD  36435  olm01  36442  olm02  36443  omlop  36447  meetat  36502  hlop  36568  polatN  37137
 Copyright terms: Public domain W3C validator