![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > olop | Structured version Visualization version GIF version |
Description: An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.) |
Ref | Expression |
---|---|
olop | ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isolat 35287 | . 2 ⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP)) | |
2 | 1 | simprbi 492 | 1 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2166 Latclat 17398 OPcops 35247 OLcol 35249 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-in 3805 df-ol 35253 |
This theorem is referenced by: olposN 35290 oldmm1 35292 oldmm2 35293 oldmm3N 35294 oldmm4 35295 oldmj1 35296 oldmj2 35297 oldmj3 35298 oldmj4 35299 olj01 35300 olj02 35301 olm11 35302 olm12 35303 latmassOLD 35304 olm01 35311 olm02 35312 omlop 35316 meetat 35371 hlop 35437 polatN 36006 |
Copyright terms: Public domain | W3C validator |