Metamath Proof Explorer


Theorem chj12i

Description: A rearrangement of Hilbert lattice join. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses chj12.1 A C
chj12.2 B C
chj12.3 C C
Assertion chj12i A B C = B A C

Proof

Step Hyp Ref Expression
1 chj12.1 A C
2 chj12.2 B C
3 chj12.3 C C
4 1 2 chjcomi A B = B A
5 4 oveq1i A B C = B A C
6 1 2 3 chjassi A B C = A B C
7 2 1 3 chjassi B A C = B A C
8 5 6 7 3eqtr3i A B C = B A C