Theorem olop 40463

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Latclat 18634  OPcops 40421  OLcol 40423

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094  df-ol 40427

This theorem is used by:  olposN  40464  oldmm1  40466  oldmm2  40467  oldmm3N  40468  oldmm4  40469  oldmj1  40470  oldmj2  40471  oldmj3  40472  oldmj4  40473  olj01  40474  olj02  40475  olm11  40476  olm12  40477  latmassOLD  40478  olm01  40485  olm02  40486  omlop  40490  meetat  40545  hlop  40611  polatN  41180