Theorem 3orass 1034

Description: Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
3orass	⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Proof of Theorem 3orass

Step	Hyp	Ref	Expression
1		df-3or 1032	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 545	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 263	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 195   ∨ wo 382   ∨ w3o 1030

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

This theorem depends on definitions:  df-bi 196  df-or 384  df-3or 1032

This theorem is referenced by:  3orrot  1037  3orcoma  1039  3orcomb  1041  3mix1  1223  ecase23d  1428  3bior1fd  1430  cador  1538  moeq3  3350  sotric  4985  sotrieq  4986  isso2i  4991  ordzsl  6937  soxp  7177  wemapsolem  8338  rankxpsuc  8628  tcrank  8630  cardlim  8681  cardaleph  8795  grur1  9521  elnnz  11264  elznn0  11269  elznn  11270  elxr  11826  xrrebnd  11873  xaddf  11929  xrinfmss  12012  ssnn0fi  12646  hashv01gt1  12995  hashtpg  13121  swrdnd2  13285  tgldimor  25197  outpasch  25447  xrdifh  28932  eliccioo  28970  orngsqr  29135  elzdif0  29352  qqhval2lem  29353  3orel1  30846  dfso2  30897  socnv  30908  dfon2lem5  30936  dfon2lem6  30937  nofv  31054  nosepon  31066  nobndup  31099  ecase13d  31477  elicc3  31481  wl-exeq  32500  dvasin  32666  4atlem3a  33901  4atlem3b  33902  frege133d  37076  or3or  37339  3ornot23VD  38104  xrssre  38505  elfzlmr  40366