Theorem olop 39213

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18337  OPcops 39171  OLcol 39173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-in 3910  df-ol 39177

This theorem is referenced by:  olposN  39214  oldmm1  39216  oldmm2  39217  oldmm3N  39218  oldmm4  39219  oldmj1  39220  oldmj2  39221  oldmj3  39222  oldmj4  39223  olj01  39224  olj02  39225  olm11  39226  olm12  39227  latmassOLD  39228  olm01  39235  olm02  39236  omlop  39240  meetat  39295  hlop  39361  polatN  39930