Theorem or32 75

Description: Swap disjuncts.

Assertion

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

Proof of Theorem or32

Step	Hyp	Ref	Expression
1		ax-a2 30	. . 3 (b v c) = (c v b)
2	1	lor 66	. 2 (a v (b v c)) = (a v (c v b))
3		ax-a3 31	. 2 ((a v b) v c) = (a v (b v c))
4		ax-a3 31	. 2 ((a v c) v b) = (a v (c v b))
5	2, 3, 4	3tr1 60	1 ((a v b) v c) = ((a v c) v b)

Syntax hints:   = wb 1   v wo 6

This theorem is referenced by:  womle2a 287  ska2 414  i3bi 478  dfi4b 482  lem4 493  ud4lem1c 561  ud4lem1 563  ud4lem2 564  ud5lem1 571  u4lemoa 605  u1lemona 607  u3lemona 609  u4lemona 610  u1lemob 612  u2lemob 613  u3lemob 614  u4lemob 615  u1lemonb 617  u2lemonb 618  u3lemonb 619  u4lem4 741  u4lem5 746  u4lem6 750  u5lem6 751  u12lem 753  u1lem11 762  3vth9 794  2oalem1 807  sadm3 820  marsdenlem2 863  oa4to6lem2 941  oa3-6lem 960  oa3-u2 972  4oath1 1020  4oagen1 1021  4oadist 1023

This theorem was proved from axioms:  ax-a2 30  ax-a3 31  ax-r1 34  ax-r2 35  ax-r5 37

metamath.org