Theorem olop 40314

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Latclat 18605  OPcops 40272  OLcol 40274

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4091  df-ol 40278

This theorem is used by:  olposN  40315  oldmm1  40317  oldmm2  40318  oldmm3N  40319  oldmm4  40320  oldmj1  40321  oldmj2  40322  oldmj3  40323  oldmj4  40324  olj01  40325  olj02  40326  olm11  40327  olm12  40328  latmassOLD  40329  olm01  40336  olm02  40337  omlop  40341  meetat  40396  hlop  40462  polatN  41031