Metamath Proof Explorer


Theorem shjcomi

Description: Commutative law for join in SH . (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 shincl.1
 |-  A e. SH
2 shincl.2
 |-  B e. SH
3 shjcom
 |-  ( ( A e. SH /\ B e. SH ) -> ( A vH B ) = ( B vH A ) )
4 1 2 3 mp2an
 |-  ( A vH B ) = ( B vH A )