Theorem 3orrot

Description: Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995)

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

Proof

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