Theorem olop 35289

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

Syntax hints:   → wi 4   ∈ wcel 2166  Latclat 17398  OPcops 35247  OLcol 35249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-ol 35253

This theorem is referenced by:  olposN  35290  oldmm1  35292  oldmm2  35293  oldmm3N  35294  oldmm4  35295  oldmj1  35296  oldmj2  35297  oldmj3  35298  oldmj4  35299  olj01  35300  olj02  35301  olm11  35302  olm12  35303  latmassOLD  35304  olm01  35311  olm02  35312  omlop  35316  meetat  35371  hlop  35437  polatN  36006