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 AC
chjcl.2 BC
Assertion chjcomi AB=BA

Proof

Step Hyp Ref Expression
1 ch0le.1 AC
2 chjcl.2 BC
3 1 chshii AS
4 2 chshii BS
5 3 4 shjcomi AB=BA