Theorem orcom 73

Description: Commutative law.

Assertion

Ref	Expression
orcom	(a ∪ b) = (b ∪ a)

Proof of Theorem orcom

Step	Hyp	Ref	Expression
1		ax-a2 31	1 (a ∪ b) = (b ∪ a)

Syntax hints:   = wb 1   ∪ wo 6

This theorem is referenced by:  k1-7 354  k1-8b 356  k1-5 360

This theorem was proved from axioms:  ax-a2 31

Copyright terms: Public domain