Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  olop Unicode version

Theorem olop 29404
Description: An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
olop  |-  ( K  e.  OL  ->  K  e.  OP )

Proof of Theorem olop
StepHypRef Expression
1 isolat 29402 . 2  |-  ( K  e.  OL  <->  ( K  e.  Lat  /\  K  e.  OP ) )
21simprbi 450 1  |-  ( K  e.  OL  ->  K  e.  OP )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   Latclat 14151   OPcops 29362   OLcol 29364
This theorem is referenced by:  olposN  29405  oldmm1  29407  oldmm2  29408  oldmm3N  29409  oldmm4  29410  oldmj1  29411  oldmj2  29412  oldmj3  29413  oldmj4  29414  olj01  29415  olj02  29416  olm11  29417  olm12  29418  latmassOLD  29419  olm01  29426  olm02  29427  omlop  29431  meetat  29486  hlop  29552  polatN  30120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ol 29368
  Copyright terms: Public domain W3C validator