Theorem olop 36342

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

Syntax hints:   → wi 4   ∈ wcel 2108  Latclat 17647  OPcops 36300  OLcol 36302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-in 3941  df-ol 36306

This theorem is referenced by:  olposN  36343  oldmm1  36345  oldmm2  36346  oldmm3N  36347  oldmm4  36348  oldmj1  36349  oldmj2  36350  oldmj3  36351  oldmj4  36352  olj01  36353  olj02  36354  olm11  36355  olm12  36356  latmassOLD  36357  olm01  36364  olm02  36365  omlop  36369  meetat  36424  hlop  36490  polatN  37059