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

Step	Hyp	Ref	Expression
1		isolat 29402	. 2 |- ( K e. OL <-> ( K e. Lat /\ K e. OP ) )
2	1	simprbi 450	1 |- ( K e. OL -> K e. OP )

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