Theorem olop 39660

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 18397  OPcops 39618  OLcol 39620

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-ol 39624

This theorem is referenced by:  olposN  39661  oldmm1  39663  oldmm2  39664  oldmm3N  39665  oldmm4  39666  oldmj1  39667  oldmj2  39668  oldmj3  39669  oldmj4  39670  olj01  39671  olj02  39672  olm11  39673  olm12  39674  latmassOLD  39675  olm01  39682  olm02  39683  omlop  39687  meetat  39742  hlop  39808  polatN  40377