![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ollat | Structured version Visualization version GIF version |
Description: An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.) |
Ref | Expression |
---|---|
ollat | ⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isolat 39194 | . 2 ⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP)) | |
2 | 1 | simplbi 497 | 1 ⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 Latclat 18489 OPcops 39154 OLcol 39156 |
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 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-in 3970 df-ol 39160 |
This theorem is referenced by: oldmm1 39199 oldmj1 39203 olj01 39207 olj02 39208 olm12 39210 latmassOLD 39211 latm12 39212 latm32 39213 latmrot 39214 latm4 39215 latmmdiN 39216 latmmdir 39217 olm01 39218 olm02 39219 omllat 39224 meetat 39278 |
Copyright terms: Public domain | W3C validator |