Theorem olop 40016

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Latclat 18493  OPcops 39974  OLcol 39976

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-ol 39980

This theorem is used by:  olposN  40017  oldmm1  40019  oldmm2  40020  oldmm3N  40021  oldmm4  40022  oldmj1  40023  oldmj2  40024  oldmj3  40025  oldmj4  40026  olj01  40027  olj02  40028  olm11  40029  olm12  40030  latmassOLD  40031  olm01  40038  olm02  40039  omlop  40043  meetat  40098  hlop  40164  polatN  40733