Metamath Proof Explorer


Theorem shjcl

Description: Closure of join in SH . (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion shjcl ASBSABC

Proof

Step Hyp Ref Expression
1 shss ASA
2 shss BSB
3 sshjcl ABABC
4 1 2 3 syl2an ASBSABC