Theorem olop 39215

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

Syntax hints:   → wi 4   ∈ wcel 2108  Latclat 18476  OPcops 39173  OLcol 39175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ol 39179

This theorem is referenced by:  olposN  39216  oldmm1  39218  oldmm2  39219  oldmm3N  39220  oldmm4  39221  oldmj1  39222  oldmj2  39223  oldmj3  39224  oldmj4  39225  olj01  39226  olj02  39227  olm11  39228  olm12  39229  latmassOLD  39230  olm01  39237  olm02  39238  omlop  39242  meetat  39297  hlop  39363  polatN  39933