Theorem olop 39509

Description: An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.)

Assertion

Ref	Expression
olop	⊢ (𝐾 ∈ OL → 𝐾 ∈ OP)

Proof of Theorem olop

Step	Hyp	Ref	Expression
1		isolat 39507	. 2 ⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
2	1	simprbi 496	1 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP)

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 18356  OPcops 39467  OLcol 39469

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 3441  df-in 3907  df-ol 39473

This theorem is referenced by:  olposN  39510  oldmm1  39512  oldmm2  39513  oldmm3N  39514  oldmm4  39515  oldmj1  39516  oldmj2  39517  oldmj3  39518  oldmj4  39519  olj01  39520  olj02  39521  olm11  39522  olm12  39523  latmassOLD  39524  olm01  39531  olm02  39532  omlop  39536  meetat  39591  hlop  39657  polatN  40226