Theorem 3orass 584

Description: Associative law for triple disjunction.

Assertion

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

Proof of Theorem 3orass

Step	Hyp	Ref	Expression
1		df-3or 582	. 2 |- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))
2		orass 218	. 2 |- (((ph \/ ps) \/ ch) <-> (ph \/ (ps \/ ch)))
3	1, 2	bitr 151	1 |- ((ph \/ ps \/ ch) <-> (ph \/ (ps \/ ch)))

Syntax hints:   <-> wb 127   \/ wo 195   \/ w3o 580

This theorem is referenced by:  3orrot 587  3mix1 600  ecased 643  eueq3 1430  moeq3 1432  sotric 2148  so 2152  dfwe2 2187  ordtri2or 2328  ordzsl 2366  cardlim 3657  cardaleph 3690  elnnz 4572  0z 4573  elznn0 4576

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197  df-3or 582

metamath.org