Metamath Proof Explorer


Theorem pjoml6i

Description: An equivalent of the orthomodular law. Theorem 29.13(e) of MaedaMaeda p. 132. (Contributed by NM, 30-May-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjoml2.1 A C
2 pjoml2.2 B C
3 1 choccli A C
4 3 2 chincli A B C
5 1 2 pjoml2i A B A A B = B
6 2 choccli B C
7 1 6 chub1i A A B
8 1 2 chdmm2i A B = A B
9 7 8 sseqtrri A A B
10 5 9 jctil A B A A B A A B = B
11 fveq2 x = A B x = A B
12 11 sseq2d x = A B A x A A B
13 oveq2 x = A B A x = A A B
14 13 eqeq1d x = A B A x = B A A B = B
15 12 14 anbi12d x = A B A x A x = B A A B A A B = B
16 15 rspcev A B C A A B A A B = B x C A x A x = B
17 4 10 16 sylancr A B x C A x A x = B