Theorem or4 77

Description: Swap disjuncts.

Assertion

Ref	Expression
or4	((a ∪ b) ∪ (c ∪ d)) = ((a ∪ c) ∪ (b ∪ d))

Proof of Theorem or4

Step	Hyp	Ref	Expression
1		or12 73	. . 3 (b ∪ (c ∪ d)) = (c ∪ (b ∪ d))
2	1	lor 66	. 2 (a ∪ (b ∪ (c ∪ d))) = (a ∪ (c ∪ (b ∪ d)))
3		ax-a3 31	. 2 ((a ∪ b) ∪ (c ∪ d)) = (a ∪ (b ∪ (c ∪ d)))
4		ax-a3 31	. 2 ((a ∪ c) ∪ (b ∪ d)) = (a ∪ (c ∪ (b ∪ d)))
5	2, 3, 4	3tr1 60	1 ((a ∪ b) ∪ (c ∪ d)) = ((a ∪ c) ∪ (b ∪ d))

Syntax hints:   = wb 1   ∪ wo 6

This theorem is referenced by:  orordi 104  orordir 105  cmtrcom 182  womle2a 287  wcom2or 409  com2or 465  i3con 533  ud1lem3 544  ud4lem1c 561  ud4lem1 563  ud4lem3b 566  ud5lem3 576  u4lem5 746  3vth6 791  3vded22 800

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

metamath.org