Theorem chjcom 29809

Description: Commutative law for Hilbert lattice join. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)

Assertion

Ref	Expression
chjcom	⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴))

Proof of Theorem chjcom

Step	Hyp	Ref	Expression
1		chsh 29527	. 2 ⊢ (𝐴 ∈ Cℋ → 𝐴 ∈ Sℋ )
2		chsh 29527	. 2 ⊢ (𝐵 ∈ Cℋ → 𝐵 ∈ Sℋ )
3		shjcom 29661	. 2 ⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴))
4	1, 2, 3	syl2an 595	1 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  (class class class)co 7260   S_ℋ csh 29231   C_ℋ cch 29232   ∨_ℋ chj 29236

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-hilex 29302

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3429  df-sbc 3717  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-id 5485  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-iota 6381  df-fun 6425  df-fv 6431  df-ov 7263  df-oprab 7264  df-mpo 7265  df-sh 29510  df-ch 29524  df-chj 29613

This theorem is referenced by:  chub2  29811  chlejb2  29816  chj12  29837  mddmd2  30612  dmdsl3  30618  csmdsymi  30637  mdexchi  30638  atordi  30687  atcvatlem  30688  atcvati  30689  chirredlem2  30694  chirredlem4  30696  atcvat3i  30699  atcvat4i  30700  atdmd  30701  mdsymlem3  30708  mdsymlem5  30710  mdsymlem8  30713  sumdmdlem2  30722  dmdbr5ati  30725