Theorem orcom 73

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

Assertion

Ref	Expression
orcom	(a ∪ b) = (b ∪ a)

Proof of Theorem orcom

Step	Hyp	Ref	Expression
1		ax-a2 31	1 (a ∪ b) = (b ∪ a)

Syntax hints:   = wb 1   ∪ wo 6

This theorem was proved from axioms:  ax-a2 31

This theorem is referenced by:  k1-7  354  k1-8b  356  k1-5  360  mli  1126  mlduali  1128  ml3le  1129  vneulem2  1132  vneulem6  1136  vneulem9  1139  vneulem10  1140  vneulem11  1141  vneulem16  1146  vneulemexp  1148  dp15lema  1154  dp15lemd  1157  dp53lema  1163  dp53lemc  1165  dp53leme  1167  dp53lemf  1168  dp35lemc  1175  dp35lem0  1179  dp41lemc0  1184  dp41leme  1187  dp41lemf  1188  dp41lemg  1189  dp41leml  1193  dp32  1196  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  testmod1  1214  testmod2  1215  testmod2expanded  1216  testmod3  1217