Theorem 3orcoma

Description: Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016)

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

Proof

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