This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chj4i

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

Ref Expression
Hypotheses chj12.1 
|- A e. CH
chj12.2 
|- B e. CH
chj12.3 
|- C e. CH
chj4.4 
|- D e. CH
Assertion chj4i 
|- ( ( A vH B ) vH ( C vH D ) ) = ( ( A vH C ) vH ( B vH D ) )

Proof

Step Hyp Ref Expression
1 chj12.1 
 |-  A e. CH
2 chj12.2 
 |-  B e. CH
3 chj12.3 
 |-  C e. CH
4 chj4.4 
 |-  D e. CH
5 2 3 4 chj12i 
 |-  ( B vH ( C vH D ) ) = ( C vH ( B vH D ) )
6 5 oveq2i 
 |-  ( A vH ( B vH ( C vH D ) ) ) = ( A vH ( C vH ( B vH D ) ) )
7 3 4 chjcli 
 |-  ( C vH D ) e. CH
8 1 2 7 chjassi 
 |-  ( ( A vH B ) vH ( C vH D ) ) = ( A vH ( B vH ( C vH D ) ) )
9 2 4 chjcli 
 |-  ( B vH D ) e. CH
10 1 3 9 chjassi 
 |-  ( ( A vH C ) vH ( B vH D ) ) = ( A vH ( C vH ( B vH D ) ) )
11 6 8 10 3eqtr4i 
 |-  ( ( A vH B ) vH ( C vH D ) ) = ( ( A vH C ) vH ( B vH D ) )