Theorem or32 82

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 31	. . 3 (b v c) = (c v b)
2	1	lor 70	. 2 (a v (b v c)) = (a v (c v b))
3		ax-a3 32	. 2 ((a v b) v c) = (a v (b v c))
4		ax-a3 32	. 2 ((a v c) v b) = (a v (c v b))
5	2, 3, 4	3tr1 63	1 ((a v b) v c) = ((a v c) v b)

Syntax hints:   = wb 1   v wo 6

This theorem is referenced by:  womle2a 295  ska2 432  i3bi 496  dfi4b 500  lem4 511  ud4lem1c 579  ud4lem1 581  ud4lem2 582  ud5lem1 589  u4lemoa 623  u1lemona 625  u3lemona 627  u4lemona 628  u1lemob 630  u2lemob 631  u3lemob 632  u4lemob 633  u1lemonb 635  u2lemonb 636  u3lemonb 637  u4lem4 759  u4lem5 764  u4lem6 768  u5lem6 769  u12lem 771  u1lem11 780  3vth9 812  2oalem1 825  sadm3 838  marsdenlem2 881  e2ast2 894  e2astlem1 895  oa4to6lem2 961  oa3-6lem 980  oa3-u2 992  4oath1 1040  4oagen1 1041  4oadist 1043

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