Theorem olop 39207

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18390  OPcops 39165  OLcol 39167

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 3449  df-in 3921  df-ol 39171

This theorem is referenced by:  olposN  39208  oldmm1  39210  oldmm2  39211  oldmm3N  39212  oldmm4  39213  oldmj1  39214  oldmj2  39215  oldmj3  39216  oldmj4  39217  olj01  39218  olj02  39219  olm11  39220  olm12  39221  latmassOLD  39222  olm01  39229  olm02  39230  omlop  39234  meetat  39289  hlop  39355  polatN  39925