Theorem 3orass 1086

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 1084	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 918	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 277	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 208   ∨ wo 843   ∨ w3o 1082

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 209  df-or 844  df-3or 1084

This theorem is referenced by:  3orel1  1087  3orrot  1088  3orcoma  1089  3mix1  1326  ecase23d  1469  3bior1fd  1471  cador  1608  moeq3  3706  sotric  5504  sotrieq  5505  isso2i  5511  ordzsl  7563  soxp  7826  wemapsolem  9017  rankxpsuc  9314  tcrank  9316  cardlim  9404  cardaleph  9518  grur1  10245  elnnz  11994  elznn0  11999  elznn  12000  elxr  12514  xrrebnd  12564  xaddf  12620  xrinfmss  12706  elfzlmr  13154  ssnn0fi  13356  hashv01gt1  13708  hashtpg  13846  swrdnd2  14020  pfxnd0  14053  tgldimor  26291  outpasch  26544  xrdifh  30506  eliccioo  30611  orngsqr  30881  elzdif0  31225  qqhval2lem  31226  dfso2  32994  dfon2lem5  33036  dfon2lem6  33037  nofv  33168  nosepon  33176  ecase13d  33665  elicc3  33669  wl-exeq  34778  dvasin  34982  4atlem3a  36737  4atlem3b  36738  frege133d  40116  or3or  40377  3ornot23VD  41187  xrssre  41622