Theorem 3orass 965

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 963	. 2 |- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
2		orass 756	. 2 |- ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )
3	1, 2	bitri 183	1 |- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )

Syntax hints:   <-> wb 104   \/ wo 697   \/ w3o 961

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 698

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

This theorem is referenced by:  3orrot  968  3orcomb  971  3mix1  1150  sotritric  4246  sotritrieq  4247  ordtriexmid  4437  acexmidlemcase  5769  nntri3or  6389  nntri2  6390  elnnz  9064  elznn0  9069  elznn  9070  zapne  9125  nn01to3  9409  elxr  9563  bezoutlemmain  11686