Theorem olop 39178

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 39176	. 2 ⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP))
2	1	simprbi 496	1 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP)

Syntax hints:   → wi 4   ∈ wcel 2108  Latclat 18439  OPcops 39136  OLcol 39138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-ol 39142

This theorem is referenced by:  olposN  39179  oldmm1  39181  oldmm2  39182  oldmm3N  39183  oldmm4  39184  oldmj1  39185  oldmj2  39186  oldmj3  39187  oldmj4  39188  olj01  39189  olj02  39190  olm11  39191  olm12  39192  latmassOLD  39193  olm01  39200  olm02  39201  omlop  39205  meetat  39260  hlop  39326  polatN  39896