Metamath Proof Explorer


Theorem pjoml2i

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 AC
pjoml2.2 BC
Assertion pjoml2i ABAAB=B

Proof

Step Hyp Ref Expression
1 pjoml2.1 AC
2 pjoml2.2 BC
3 inss2 ABB
4 1 choccli AC
5 4 2 chincli ABC
6 1 5 2 chlubii ABABBAABB
7 3 6 mpan2 ABAABB
8 1 5 chdmj1i AAB=AAB
9 8 ineq2i BAAB=BAAB
10 incom BA=AB
11 10 ineq1i BAAB=ABAB
12 inass BAAB=BAAB
13 5 chocini ABAB=0
14 11 12 13 3eqtr3i BAAB=0
15 9 14 eqtri BAAB=0
16 1 5 chjcli AABC
17 2 chshii BS
18 16 17 pjomli AABBBAAB=0AAB=B
19 7 15 18 sylancl ABAAB=B