Theorem 3orass 776

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 774	. 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 772

This theorem is referenced by:  3orrot 779  3mix1 813  ecase23d 919  eueq3 1910  moeq3 1912  sotric 2851  so 2855  dfwe2 2925  ordtri2or 3067  ordzsl 3106  dfrdg2 3918  rankxpsuc 4687  cardlim 4823  cardaleph 4857  elxr 5508  ssxr 5513  xrrebndt 5541  xrinfmss 6026  elnnz 6092  0z 6093  elznn0 6096  elznn 6097

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 774

Copyright terms: Public domain