Description: Value of join in CH . (Contributed by NM, 9-Aug-2000) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | chjval.1 | |- A e. CH |
|
chjval.2 | |- B e. CH |
||
Assertion | chjvali | |- ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chjval.1 | |- A e. CH |
|
2 | chjval.2 | |- B e. CH |
|
3 | chjval | |- ( ( A e. CH /\ B e. CH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) ) |
|
4 | 1 2 3 | mp2an | |- ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) |