Theorem olop 39312

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

Syntax hints:   → wi 4   ∈ wcel 2111  Latclat 18337  OPcops 39270  OLcol 39272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-ol 39276

This theorem is referenced by:  olposN  39313  oldmm1  39315  oldmm2  39316  oldmm3N  39317  oldmm4  39318  oldmj1  39319  oldmj2  39320  oldmj3  39321  oldmj4  39322  olj01  39323  olj02  39324  olm11  39325  olm12  39326  latmassOLD  39327  olm01  39334  olm02  39335  omlop  39339  meetat  39394  hlop  39460  polatN  40029