Theorem or12 80

Description: Swap disjuncts.

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  1104  ml3le  1127  l42modlem1  1147  dp15lemd  1155  dp15lemf  1157  xdp15  1197  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206