Metamath Proof Explorer


Theorem pjoml4i

Description: Variation of orthomodular law. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjoml2.1 A C
2 pjoml2.2 B C
3 inss1 B A B B
4 1 choccli A C
5 2 choccli B C
6 4 5 chjcli A B C
7 2 6 chincli B A B C
8 7 2 1 chlej2i B A B B A B A B A B
9 3 8 ax-mp A B A B A B
10 1 7 chub1i A A B A B
11 1 2 chdmm1i A B = A B
12 11 ineq1i A B B = A B B
13 incom A B B = B A B
14 12 13 eqtri A B B = B A B
15 14 oveq2i A B A B B = A B B A B
16 inss2 A B B
17 1 2 chincli A B C
18 17 2 pjoml2i A B B A B A B B = B
19 16 18 ax-mp A B A B B = B
20 15 19 eqtr3i A B B A B = B
21 inss1 A B A
22 17 1 7 chlej1i A B A A B B A B A B A B
23 21 22 ax-mp A B B A B A B A B
24 20 23 eqsstrri B A B A B
25 1 7 chjcli A B A B C
26 1 2 25 chlubii A A B A B B A B A B A B A B A B
27 10 24 26 mp2an A B A B A B
28 9 27 eqssi A B A B = A B