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

Theorem olop 29463
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 29461 . 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 1715   Latclat 14361   OPcops 29421   OLcol 29423
This theorem is referenced by:  olposN  29464  oldmm1  29466  oldmm2  29467  oldmm3N  29468  oldmm4  29469  oldmj1  29470  oldmj2  29471  oldmj3  29472  oldmj4  29473  olj01  29474  olj02  29475  olm11  29476  olm12  29477  latmassOLD  29478  olm01  29485  olm02  29486  omlop  29490  meetat  29545  hlop  29611  polatN  30179
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-in 3245  df-ol 29427
  Copyright terms: Public domain W3C validator