Theorem olop 40191

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Latclat 18566  OPcops 40149  OLcol 40151

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3905  df-ol 40155

This theorem is used by:  olposN  40192  oldmm1  40194  oldmm2  40195  oldmm3N  40196  oldmm4  40197  oldmj1  40198  oldmj2  40199  oldmj3  40200  oldmj4  40201  olj01  40202  olj02  40203  olm11  40204  olm12  40205  latmassOLD  40206  olm01  40213  olm02  40214  omlop  40218  meetat  40273  hlop  40339  polatN  40908