Theorem olop 39553

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 18359  OPcops 39511  OLcol 39513

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 3443  df-in 3909  df-ol 39517

This theorem is referenced by:  olposN  39554  oldmm1  39556  oldmm2  39557  oldmm3N  39558  oldmm4  39559  oldmj1  39560  oldmj2  39561  oldmj3  39562  oldmj4  39563  olj01  39564  olj02  39565  olm11  39566  olm12  39567  latmassOLD  39568  olm01  39575  olm02  39576  omlop  39580  meetat  39635  hlop  39701  polatN  40270