# Metamath Proof Explorer

## Theorem fh3i

Description: Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses fh1.1
`|- A e. CH`
fh1.2
`|- B e. CH`
fh1.3
`|- C e. CH`
fh1.4
`|- A C_H B`
fh1.5
`|- A C_H C`
Assertion fh3i
`|- ( A vH ( B i^i C ) ) = ( ( A vH B ) i^i ( A vH C ) )`

### Proof

Step Hyp Ref Expression
1 fh1.1
` |-  A e. CH`
2 fh1.2
` |-  B e. CH`
3 fh1.3
` |-  C e. CH`
4 fh1.4
` |-  A C_H B`
5 fh1.5
` |-  A C_H C`
6 1 choccli
` |-  ( _|_ ` A ) e. CH`
7 2 choccli
` |-  ( _|_ ` B ) e. CH`
8 3 choccli
` |-  ( _|_ ` C ) e. CH`
9 1 2 4 cmcm3ii
` |-  ( _|_ ` A ) C_H B`
10 6 2 9 cmcm2ii
` |-  ( _|_ ` A ) C_H ( _|_ ` B )`
11 1 3 5 cmcm3ii
` |-  ( _|_ ` A ) C_H C`
12 6 3 11 cmcm2ii
` |-  ( _|_ ` A ) C_H ( _|_ ` C )`
13 6 7 8 10 12 fh1i
` |-  ( ( _|_ ` A ) i^i ( ( _|_ ` B ) vH ( _|_ ` C ) ) ) = ( ( ( _|_ ` A ) i^i ( _|_ ` B ) ) vH ( ( _|_ ` A ) i^i ( _|_ ` C ) ) )`
14 2 3 chdmm1i
` |-  ( _|_ ` ( B i^i C ) ) = ( ( _|_ ` B ) vH ( _|_ ` C ) )`
15 14 ineq2i
` |-  ( ( _|_ ` A ) i^i ( _|_ ` ( B i^i C ) ) ) = ( ( _|_ ` A ) i^i ( ( _|_ ` B ) vH ( _|_ ` C ) ) )`
16 1 2 chdmj1i
` |-  ( _|_ ` ( A vH B ) ) = ( ( _|_ ` A ) i^i ( _|_ ` B ) )`
17 1 3 chdmj1i
` |-  ( _|_ ` ( A vH C ) ) = ( ( _|_ ` A ) i^i ( _|_ ` C ) )`
18 16 17 oveq12i
` |-  ( ( _|_ ` ( A vH B ) ) vH ( _|_ ` ( A vH C ) ) ) = ( ( ( _|_ ` A ) i^i ( _|_ ` B ) ) vH ( ( _|_ ` A ) i^i ( _|_ ` C ) ) )`
19 13 15 18 3eqtr4ri
` |-  ( ( _|_ ` ( A vH B ) ) vH ( _|_ ` ( A vH C ) ) ) = ( ( _|_ ` A ) i^i ( _|_ ` ( B i^i C ) ) )`
20 1 2 chjcli
` |-  ( A vH B ) e. CH`
21 1 3 chjcli
` |-  ( A vH C ) e. CH`
22 20 21 chdmm1i
` |-  ( _|_ ` ( ( A vH B ) i^i ( A vH C ) ) ) = ( ( _|_ ` ( A vH B ) ) vH ( _|_ ` ( A vH C ) ) )`
23 2 3 chincli
` |-  ( B i^i C ) e. CH`
24 1 23 chdmj1i
` |-  ( _|_ ` ( A vH ( B i^i C ) ) ) = ( ( _|_ ` A ) i^i ( _|_ ` ( B i^i C ) ) )`
25 19 22 24 3eqtr4i
` |-  ( _|_ ` ( ( A vH B ) i^i ( A vH C ) ) ) = ( _|_ ` ( A vH ( B i^i C ) ) )`
26 1 23 chjcli
` |-  ( A vH ( B i^i C ) ) e. CH`
27 20 21 chincli
` |-  ( ( A vH B ) i^i ( A vH C ) ) e. CH`
28 26 27 chcon3i
` |-  ( ( A vH ( B i^i C ) ) = ( ( A vH B ) i^i ( A vH C ) ) <-> ( _|_ ` ( ( A vH B ) i^i ( A vH C ) ) ) = ( _|_ ` ( A vH ( B i^i C ) ) ) )`
29 25 28 mpbir
` |-  ( A vH ( B i^i C ) ) = ( ( A vH B ) i^i ( A vH C ) )`