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 36340 | . 2 ⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP)) | |
2 | 1 | simprbi 499 | 1 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2108 Latclat 17647 OPcops 36300 OLcol 36302 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-v 3495 df-in 3941 df-ol 36306 |
This theorem is referenced by: olposN 36343 oldmm1 36345 oldmm2 36346 oldmm3N 36347 oldmm4 36348 oldmj1 36349 oldmj2 36350 oldmj3 36351 oldmj4 36352 olj01 36353 olj02 36354 olm11 36355 olm12 36356 latmassOLD 36357 olm01 36364 olm02 36365 omlop 36369 meetat 36424 hlop 36490 polatN 37059 |
Copyright terms: Public domain | W3C validator |