Metamath Proof Explorer


Theorem chjcomi

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

Ref Expression
Hypotheses ch0le.1 A C
chjcl.2 B C
Assertion chjcomi A B = B A

Proof

Step Hyp Ref Expression
1 ch0le.1 A C
2 chjcl.2 B C
3 1 chshii A S
4 2 chshii B S
5 3 4 shjcomi A B = B A