Metamath Proof Explorer


Theorem pjoml3i

Description: Variation of orthomodular law. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 A C
pjoml2.2 B C
Assertion pjoml3i B A A A B = B

Proof

Step Hyp Ref Expression
1 pjoml2.1 A C
2 pjoml2.2 B C
3 1 choccli A C
4 2 choccli B C
5 3 4 pjoml2i A B A A B = B
6 2 1 chsscon3i B A A B
7 eqcom A A B = B B = A A B
8 3 choccli A C
9 8 4 chincli A B C
10 1 9 chdmj2i A A B = A A B
11 3 2 chdmm4i A B = A B
12 11 ineq2i A A B = A A B
13 10 12 eqtri A A B = A A B
14 13 eqeq1i A A B = B A A B = B
15 3 9 chjcli A A B C
16 2 15 chcon2i B = A A B A A B = B
17 7 14 16 3bitr3i A A B = B A A B = B
18 5 6 17 3imtr4i B A A A B = B