Theorem olop 40074

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Latclat 18523  OPcops 40032  OLcol 40034

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909  df-ol 40038

This theorem is used by:  olposN  40075  oldmm1  40077  oldmm2  40078  oldmm3N  40079  oldmm4  40080  oldmj1  40081  oldmj2  40082  oldmj3  40083  oldmj4  40084  olj01  40085  olj02  40086  olm11  40087  olm12  40088  latmassOLD  40089  olm01  40096  olm02  40097  omlop  40101  meetat  40156  hlop  40222  polatN  40791