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 𝐴S
shincl.2 𝐵S
Assertion shjshcli ( 𝐴 𝐵 ) ∈ S

Proof

Step Hyp Ref Expression
1 shincl.1 𝐴S
2 shincl.2 𝐵S
3 1 2 shjcli ( 𝐴 𝐵 ) ∈ C
4 3 chshii ( 𝐴 𝐵 ) ∈ S