Theorem or12 80

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

Assertion

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

Proof of Theorem or12

Step	Hyp	Ref	Expression
1		ax-a2 31	. . 3 (a ∪ b) = (b ∪ a)
2	1	ax-r5 38	. 2 ((a ∪ b) ∪ c) = ((b ∪ a) ∪ c)
3		ax-a3 32	. 2 ((a ∪ b) ∪ c) = (a ∪ (b ∪ c))
4		ax-a3 32	. 2 ((b ∪ a) ∪ c) = (b ∪ (a ∪ c))
5	2, 3, 4	3tr2 64	1 (a ∪ (b ∪ c)) = (b ∪ (a ∪ c))

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:  or4  84  sklem  230  nom21  314  nom22  315  ska2  432  woml6  436  oml5  449  i0cmtrcom  495  df2i3  498  i3con  551  ud1lem1  560  ud3lem1c  568  ud3lem1  570  ud3lem3  576  ud5lem3  594  u3lemob  632  u4lemob  633  u4lem6  768  u3lem7  774  u1lem11  780  test  802  3vth5  808  3vth7  810  3vth9  812  3vded22  818  2oalem1  825  3vroa  831  orbi  842  mhlem  876  mh  879  oa3-2lemb  979  oa3-5lem  984  mloa  1018  wdwom  1106  ml3le  1129  l42modlem1  1149  dp15lemd  1157  dp15lemf  1159  xdp15  1199  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208