Theorem or32 82

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

Assertion

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

Proof of Theorem or32

Step	Hyp	Ref	Expression
1		ax-a2 31	. . 3 (b ∪ c) = (c ∪ b)
2	1	lor 70	. 2 (a ∪ (b ∪ c)) = (a ∪ (c ∪ b))
3		ax-a3 32	. 2 ((a ∪ b) ∪ c) = (a ∪ (b ∪ c))
4		ax-a3 32	. 2 ((a ∪ c) ∪ b) = (a ∪ (c ∪ b))
5	2, 3, 4	3tr1 63	1 ((a ∪ b) ∪ c) = ((a ∪ c) ∪ b)

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:  womle2a  295  ska2  432  i3bi  496  dfi4b  500  lem4  511  ud4lem1c  579  ud4lem1  581  ud4lem2  582  ud5lem1  589  u4lemoa  623  u1lemona  625  u3lemona  627  u4lemona  628  u1lemob  630  u2lemob  631  u3lemob  632  u4lemob  633  u1lemonb  635  u2lemonb  636  u3lemonb  637  u4lem4  759  u4lem5  764  u4lem6  768  u5lem6  769  u12lem  771  u1lem11  780  3vth9  812  2oalem1  825  sadm3  838  marsdenlem2  881  e2ast2  894  e2astlem1  895  oa4to6lem2  961  oa3-6lem  980  oa3-u2  992  4oath1  1041  4oagen1  1042  4oadist  1044  vneulem6  1136  vneulem10  1140  vneulem11  1141  vneulemexp  1148  dp15lema  1154  dp53lemc  1165  dp35lemc  1175  dp41lemc0  1184  dp41lemg  1189  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemc  1211  testmod  1213