Theorem or12 73

Description: Swap disjuncts.

Assertion

Ref	Expression
or12	(a ∪ (b ∪ c)) = (b ∪ (a ∪ c))

Proof of Theorem or12

Step	Hyp	Ref	Expression
1		ax-a2 30	. . 3 (a ∪ b) = (b ∪ a)
2	1	ax-r5 37	. 2 ((a ∪ b) ∪ c) = ((b ∪ a) ∪ c)
3		ax-a3 31	. 2 ((a ∪ b) ∪ c) = (a ∪ (b ∪ c))
4		ax-a3 31	. 2 ((b ∪ a) ∪ c) = (b ∪ (a ∪ c))
5	2, 3, 4	3tr2 61	1 (a ∪ (b ∪ c)) = (b ∪ (a ∪ c))

Syntax hints:   = wb 1   ∪ wo 6

This theorem is referenced by:  or4 77  sklem 222  nom21 306  nom22 307  ska2 414  woml6 418  oml5 431  i0cmtrcom 477  df2i3 480  i3con 533  ud1lem1 542  ud3lem1c 550  ud3lem1 552  ud3lem3 558  ud5lem3 576  u3lemob 614  u4lemob 615  u4lem6 750  u3lem7 756  u1lem11 762  test 784  3vth5 790  3vth7 792  3vth9 794  3vded22 800  2oalem1 807  3vroa 813  orbi 824  mhlem 858  mh 861  oa3-2lemb 959  oa3-5lem 964  mloa 998

This theorem was proved from axioms:  ax-a2 30  ax-a3 31  ax-r1 34  ax-r2 35  ax-r5 37

metamath.org