Theorem olop 39776

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

Syntax hints:   → wi 4   ∈ wcel 2132  Latclat 18435  OPcops 39734  OLcol 39736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-v 3446  df-in 3902  df-ol 39740

This theorem is referenced by:  olposN  39777  oldmm1  39779  oldmm2  39780  oldmm3N  39781  oldmm4  39782  oldmj1  39783  oldmj2  39784  oldmj3  39785  oldmj4  39786  olj01  39787  olj02  39788  olm11  39789  olm12  39790  latmassOLD  39791  olm01  39798  olm02  39799  omlop  39803  meetat  39858  hlop  39924  polatN  40493