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 ACBCCCDCABCD=ACBD

Proof

Step Hyp Ref Expression
1 chj12 BCCCDCBCD=CBD
2 1 3expb BCCCDCBCD=CBD
3 2 adantll ACBCCCDCBCD=CBD
4 3 oveq2d ACBCCCDCABCD=ACBD
5 chjcl CCDCCDC
6 chjass ACBCCDCABCD=ABCD
7 6 3expa ACBCCDCABCD=ABCD
8 5 7 sylan2 ACBCCCDCABCD=ABCD
9 chjcl BCDCBDC
10 chjass ACCCBDCACBD=ACBD
11 10 3expa ACCCBDCACBD=ACBD
12 9 11 sylan2 ACCCBCDCACBD=ACBD
13 12 an4s ACBCCCDCACBD=ACBD
14 4 8 13 3eqtr4d ACBCCCDCABCD=ACBD