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  4254  sotritrieq  4255  ordtriexmid  4445  acexmidlemcase  5777  nntri3or  6397  nntri2  6398  elnnz  9088  elznn0  9093  elznn  9094  zapne  9149  nn01to3  9436  elxr  9593  bezoutlemmain  11722