Theorem or4 84

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 80	. . 3 (b ∪ (c ∪ d)) = (c ∪ (b ∪ d))
2	1	lor 70	. 2 (a ∪ (b ∪ (c ∪ d))) = (a ∪ (c ∪ (b ∪ d)))
3		ax-a3 32	. 2 ((a ∪ b) ∪ (c ∪ d)) = (a ∪ (b ∪ (c ∪ d)))
4		ax-a3 32	. 2 ((a ∪ c) ∪ (b ∪ d)) = (a ∪ (c ∪ (b ∪ d)))
5	2, 3, 4	3tr1 63	1 ((a ∪ b) ∪ (c ∪ d)) = ((a ∪ c) ∪ (b ∪ d))

Syntax hints:   = wb 1   ∪ wo 6

This theorem is referenced by:  or42 85  orordi 112  orordir 113  cmtrcom 190  womle2a 295  k1-2 357  k1-3 358  wcom2or 427  com2or 483  i3con 551  ud1lem3 562  ud4lem1c 579  ud4lem1 581  ud4lem3b 584  ud5lem3 594  u4lem5 764  3vth6 809  3vded22 818  wdwom 1103

This theorem was proved from axioms:  ax-a2 31  ax-a3 32  ax-r1 35  ax-r2 36  ax-r5 38

Copyright terms: Public domain