Theorem 3orass 966

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

Assertion

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

Proof of Theorem 3orass

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

Syntax hints:   <-> wb 104   \/ wo 698   \/ w3o 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116  df-3or 964

This theorem is referenced by:  3orrot  969  3orcomb  972  3mix1  1151  sotritric  4279  sotritrieq  4280  ordtriexmid  4474  ontriexmidim  4475  acexmidlemcase  5809  nntri3or  6429  nntri2  6430  exmidontriimlem1  7135  elnnz  9156  elznn0  9161  elznn  9162  zapne  9217  nn01to3  9504  elxr  9661  bezoutlemmain  11853