![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > Mathboxes > olop | Unicode version |
Description: An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.) |
Ref | Expression |
---|---|
olop |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isolat 29707 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simprbi 451 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: olposN 29710 oldmm1 29712 oldmm2 29713 oldmm3N 29714 oldmm4 29715 oldmj1 29716 oldmj2 29717 oldmj3 29718 oldmj4 29719 olj01 29720 olj02 29721 olm11 29722 olm12 29723 latmassOLD 29724 olm01 29731 olm02 29732 omlop 29736 meetat 29791 hlop 29857 polatN 30425 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2393 |
This theorem depends on definitions: df-bi 178 df-an 361 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-clab 2399 df-cleq 2405 df-clel 2408 df-nfc 2537 df-v 2926 df-in 3295 df-ol 29673 |
Copyright terms: Public domain | W3C validator |