Theorem olop 38176

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

Syntax hints:   → wi 4   ∈ wcel 2106  Latclat 18386  OPcops 38134  OLcol 38136

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ol 38140

This theorem is referenced by:  olposN  38177  oldmm1  38179  oldmm2  38180  oldmm3N  38181  oldmm4  38182  oldmj1  38183  oldmj2  38184  oldmj3  38185  oldmj4  38186  olj01  38187  olj02  38188  olm11  38189  olm12  38190  latmassOLD  38191  olm01  38198  olm02  38199  omlop  38203  meetat  38258  hlop  38324  polatN  38894