Theorem olop 39200

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18372  OPcops 39158  OLcol 39160

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 3446  df-in 3918  df-ol 39164

This theorem is referenced by:  olposN  39201  oldmm1  39203  oldmm2  39204  oldmm3N  39205  oldmm4  39206  oldmj1  39207  oldmj2  39208  oldmj3  39209  oldmj4  39210  olj01  39211  olj02  39212  olm11  39213  olm12  39214  latmassOLD  39215  olm01  39222  olm02  39223  omlop  39227  meetat  39282  hlop  39348  polatN  39918