Metamath Proof Explorer


Theorem chj4

Description: Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion chj4 A C B C C C D C A B C D = A C B D

Proof

Step Hyp Ref Expression
1 chj12 B C C C D C B C D = C B D
2 1 3expb B C C C D C B C D = C B D
3 2 adantll A C B C C C D C B C D = C B D
4 3 oveq2d A C B C C C D C A B C D = A C B D
5 chjcl C C D C C D C
6 chjass A C B C C D C A B C D = A B C D
7 6 3expa A C B C C D C A B C D = A B C D
8 5 7 sylan2 A C B C C C D C A B C D = A B C D
9 chjcl B C D C B D C
10 chjass A C C C B D C A C B D = A C B D
11 10 3expa A C C C B D C A C B D = A C B D
12 9 11 sylan2 A C C C B C D C A C B D = A C B D
13 12 an4s A C B C C C D C A C B D = A C B D
14 4 8 13 3eqtr4d A C B C C C D C A B C D = A C B D