Theorem olop 39934

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

Syntax hints:   → wi 4   ∈ wcel 2141  Latclat 18486  OPcops 39892  OLcol 39894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911  df-ol 39898

This theorem is referenced by:  olposN  39935  oldmm1  39937  oldmm2  39938  oldmm3N  39939  oldmm4  39940  oldmj1  39941  oldmj2  39942  oldmj3  39943  oldmj4  39944  olj01  39945  olj02  39946  olm11  39947  olm12  39948  latmassOLD  39949  olm01  39956  olm02  39957  omlop  39961  meetat  40016  hlop  40082  polatN  40651