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 36342 | . 2 ⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP)) | |
2 | 1 | simprbi 499 | 1 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 Latclat 17649 OPcops 36302 OLcol 36304 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-in 3942 df-ol 36308 |
This theorem is referenced by: olposN 36345 oldmm1 36347 oldmm2 36348 oldmm3N 36349 oldmm4 36350 oldmj1 36351 oldmj2 36352 oldmj3 36353 oldmj4 36354 olj01 36355 olj02 36356 olm11 36357 olm12 36358 latmassOLD 36359 olm01 36366 olm02 36367 omlop 36371 meetat 36426 hlop 36492 polatN 37061 |
Copyright terms: Public domain | W3C validator |