Theorem orass 75

Description: Associative law.

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  1140  vneulemexp  1146  l42modlem1  1147  dp15lema  1152  dp15lemd  1155  dp15leme  1156  dp15lemg  1158  dp53leme  1165  dp35lemd  1172  dp34  1179  dp41lemc0  1182  dp41lemj  1189  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  testmod  1211  testmod2  1213  testmod2expanded  1214