Theorem orass 75

Description: Associative law. (Contributed by NM, 27-May-2008.) (Revised by NM, 31-Mar-2011.)

Assertion

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

Proof of Theorem orass

Step	Hyp	Ref	Expression
1		ax-a3 32	1 ((a ∪ b) ∪ c) = (a ∪ (b ∪ c))

Syntax hints:   = wb 1   ∪ wo 6

This theorem was proved from axioms:  ax-a3 32

This theorem is referenced by:  oa3moa3  1029  vneulem12  1142  vneulemexp  1148  l42modlem1  1149  dp15lema  1154  dp15lemd  1157  dp15leme  1158  dp15lemg  1160  dp53leme  1167  dp35lemd  1174  dp34  1181  dp41lemc0  1184  dp41lemj  1191  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod  1213  testmod2  1215  testmod2expanded  1216