Description: Variation of orthomodular law. Definition in Kalmbach p. 22. (Contributed by NM, 31-Oct-2000) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pjoml2.1 | |
|
pjoml2.2 | |
||
Assertion | pjoml2i | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjoml2.1 | |
|
2 | pjoml2.2 | |
|
3 | inss2 | |
|
4 | 1 | choccli | |
5 | 4 2 | chincli | |
6 | 1 5 2 | chlubii | |
7 | 3 6 | mpan2 | |
8 | 1 5 | chdmj1i | |
9 | 8 | ineq2i | |
10 | incom | |
|
11 | 10 | ineq1i | |
12 | inass | |
|
13 | 5 | chocini | |
14 | 11 12 13 | 3eqtr3i | |
15 | 9 14 | eqtri | |
16 | 1 5 | chjcli | |
17 | 2 | chshii | |
18 | 16 17 | pjomli | |
19 | 7 15 18 | sylancl | |