Metamath Proof Explorer


Theorem shjcli

Description: Closure of CH join. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1 AS
shincl.2 BS
Assertion shjcli ABC

Proof

Step Hyp Ref Expression
1 shincl.1 AS
2 shincl.2 BS
3 shjcl ASBSABC
4 1 2 3 mp2an ABC