Theorem or12 80

Description: Swap disjuncts.

Assertion

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

Proof of Theorem or12

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

Syntax hints:   = wb 1   v wo 6

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 1103

This theorem was proved from axioms:  ax-a2 31  ax-a3 32  ax-r1 35  ax-r2 36  ax-r5 38

Copyright terms: Public domain