Theorem 3orass 1089

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 1087	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 919	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 274	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 205   ∨ wo 844   ∨ w3o 1085

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 206  df-or 845  df-3or 1087

This theorem is referenced by:  3orel1  1090  3orrot  1091  3orcoma  1092  3mix1  1329  ecase23d  1472  3bior1fd  1474  cador  1610  moeq3  3647  sotric  5527  sotrieq  5528  isso2i  5534  ordzsl  7683  soxp  7958  wemapsolem  9297  rankxpsuc  9628  tcrank  9630  cardlim  9718  cardaleph  9833  grur1  10564  elnnz  12317  elznn0  12322  elznn  12323  elxr  12840  xrrebnd  12890  xaddf  12946  xrinfmss  13032  elfzlmr  13489  ssnn0fi  13693  hashv01gt1  14047  hashtpg  14187  swrdnd2  14356  pfxnd0  14389  tgldimor  26851  outpasch  27104  xrdifh  31087  eliccioo  31191  orngsqr  31489  elzdif0  31916  qqhval2lem  31917  dfso2  33708  dfon2lem5  33749  dfon2lem6  33750  frxp3  33783  nofv  33846  nosepon  33854  ecase13d  34488  elicc3  34492  wl-df4-3mintru2  35644  wl-exeq  35679  dvasin  35847  4atlem3a  37597  4atlem3b  37598  frege133d  41332  or3or  41590  3ornot23VD  42426  xrssre  42846