Theorem 3orass 777

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 775	. 2 |- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))
2		orass 260	. 2 |- (((ph \/ ps) \/ ch) <-> (ph \/ (ps \/ ch)))
3	1, 2	bitr 173	1 |- ((ph \/ ps \/ ch) <-> (ph \/ (ps \/ ch)))

Syntax hints:   <-> wb 146   \/ wo 222   \/ w3o 773

This theorem is referenced by:  3orrot 780  3mix1 814  ecase23d 920  eueq3 1915  moeq3 1917  sotric 2855  so 2859  dfwe2 2930  ordtri2or 3072  ordzsl 3111  dfrdg2 3924  rankxpsuc 4695  cardlim 4831  cardaleph 4865  elxr 5516  ssxr 5521  xrrebndt 5549  xrinfmss 6034  elnnz 6100  0z 6101  elznn0 6104  elznn 6105

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

This theorem depends on definitions:  df-bi 147  df-or 224  df-3or 775

Copyright terms: Public domain