Theorem orass 75

Description: Associative law.

Assertion

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

Proof of Theorem orass

Step	Hyp	Ref	Expression
1		ax-a3 32	1 ((a v b) v c) = (a v (b v c))

Syntax hints:   = wb 1   v wo 6

This theorem was proved from axioms:  ax-a3 32

Copyright terms: Public domain