Theorem olop 39843

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

Syntax hints:   → wi 4   ∈ wcel 2143  Latclat 18473  OPcops 39801  OLcol 39803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-ol 39807

This theorem is referenced by:  olposN  39844  oldmm1  39846  oldmm2  39847  oldmm3N  39848  oldmm4  39849  oldmj1  39850  oldmj2  39851  oldmj3  39852  oldmj4  39853  olj01  39854  olj02  39855  olm11  39856  olm12  39857  latmassOLD  39858  olm01  39865  olm02  39866  omlop  39870  meetat  39925  hlop  39991  polatN  40560