Theorem 3orass

Description: Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994)

	Ref	Expression
Assertion	3orass	|- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-3or	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
2		orass	|- ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )
3	1 2	bitri	|- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )