Theorem olop 39651

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 18355  OPcops 39609  OLcol 39611

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 39615

This theorem is referenced by:  olposN  39652  oldmm1  39654  oldmm2  39655  oldmm3N  39656  oldmm4  39657  oldmj1  39658  oldmj2  39659  oldmj3  39660  oldmj4  39661  olj01  39662  olj02  39663  olm11  39664  olm12  39665  latmassOLD  39666  olm01  39673  olm02  39674  omlop  39678  meetat  39733  hlop  39799  polatN  40368