Theorem or4 84

Description: Swap disjuncts. (Contributed by NM, 27-Aug-1997.)

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 was proved from axioms:  ax-a2 31  ax-a3 32  ax-r1 35  ax-r2 36  ax-r5 38

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  1106  dp41lemf  1188  dp41leml  1193  xdp41  1198  xxdp41  1201  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208