Metamath Proof Explorer


Theorem shjshcli

Description: SH closure of join. (Contributed by NM, 5-May-2000) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1
|- A e. SH
shincl.2
|- B e. SH
Assertion shjshcli
|- ( A vH B ) e. SH

Proof

Step Hyp Ref Expression
1 shincl.1
 |-  A e. SH
2 shincl.2
 |-  B e. SH
3 1 2 shjcli
 |-  ( A vH B ) e. CH
4 3 chshii
 |-  ( A vH B ) e. SH