Theorem orcom 73

Description: Commutative law.

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  1124  mlduali  1126  ml3le  1127  vneulem2  1130  vneulem6  1134  vneulem9  1137  vneulem10  1138  vneulem11  1139  vneulem16  1144  vneulemexp  1146  dp15lema  1152  dp15lemd  1155  dp53lema  1161  dp53lemc  1163  dp53leme  1165  dp53lemf  1166  dp35lemc  1173  dp35lem0  1177  dp41lemc0  1182  dp41leme  1185  dp41lemf  1186  dp41lemg  1187  dp41leml  1191  dp32  1194  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  oadp35lemc  1209  testmod  1211  testmod1  1212  testmod2  1213  testmod2expanded  1214  testmod3  1215