Theorem 3orass 983

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 981	. 2 |- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
2		orass 768	. 2 |- ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )
3	1, 2	bitri 184	1 |- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )

Syntax hints:   <-> wb 105   \/ wo 709   \/ w3o 979

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

This theorem depends on definitions:  df-bi 117  df-3or 981

This theorem is referenced by:  3orrot  986  3orcomb  989  3mix1  1168  sotritric  4356  sotritrieq  4357  ordtriexmid  4554  ontriexmidim  4555  acexmidlemcase  5914  nntri3or  6548  nntri2  6549  exmidontriimlem1  7283  elnnz  9330  elznn0  9335  elznn  9336  zapne  9394  nn01to3  9685  elxr  9845  bezoutlemmain  12138  nninfctlemfo  12180  lgsdilem  15184  gausslemma2dlem4  15221