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  1609  moeq3  3703  sotric  5501  sotrieq  5502  isso2i  5508  ordzsl  7560  soxp  7823  wemapsolem  9014  rankxpsuc  9311  tcrank  9313  cardlim  9401  cardaleph  9515  grur1  10242  elnnz  11992  elznn0  11997  elznn  11998  elxr  12512  xrrebnd  12562  xaddf  12618  xrinfmss  12704  elfzlmr  13152  ssnn0fi  13354  hashv01gt1  13706  hashtpg  13844  swrdnd2  14017  pfxnd0  14050  tgldimor  26288  outpasch  26541  xrdifh  30503  eliccioo  30607  orngsqr  30877  elzdif0  31221  qqhval2lem  31222  dfso2  32990  dfon2lem5  33032  dfon2lem6  33033  nofv  33164  nosepon  33172  ecase13d  33661  elicc3  33665  wl-exeq  34789  dvasin  34993  4atlem3a  36748  4atlem3b  36749  frege133d  40159  or3or  40420  3ornot23VD  41230  xrssre  41665