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 S
shincl.2 B S
Assertion shjshcli A B S

Proof

Step Hyp Ref Expression
1 shincl.1 A S
2 shincl.2 B S
3 1 2 shjcli A B C
4 3 chshii A B S