Theorem olop 36510

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

Syntax hints:   → wi 4   ∈ wcel 2111  Latclat 17647  OPcops 36468  OLcol 36470

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ol 36474

This theorem is referenced by:  olposN  36511  oldmm1  36513  oldmm2  36514  oldmm3N  36515  oldmm4  36516  oldmj1  36517  oldmj2  36518  oldmj3  36519  oldmj4  36520  olj01  36521  olj02  36522  olm11  36523  olm12  36524  latmassOLD  36525  olm01  36532  olm02  36533  omlop  36537  meetat  36592  hlop  36658  polatN  37227