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  1104  dp41lemf  1186  dp41leml  1191  xdp41  1196  xxdp41  1199  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206