Theorem 3orass 1040

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 1038	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 546	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 264	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 196   ∨ wo 383   ∨ w3o 1036

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 197  df-or 385  df-3or 1038

This theorem is referenced by:  3orel1  1041  3orrot  1044  3orcoma  1046  3orcomb  1048  3mix1  1230  ecase23d  1436  3bior1fd  1438  cador  1547  moeq3  3383  sotric  5061  sotrieq  5062  isso2i  5067  ordzsl  7045  soxp  7290  wemapsolem  8455  rankxpsuc  8745  tcrank  8747  cardlim  8798  cardaleph  8912  grur1  9642  elnnz  11387  elznn0  11392  elznn  11393  elxr  11950  xrrebnd  11999  xaddf  12055  xrinfmss  12140  elfzlmr  12582  ssnn0fi  12784  hashv01gt1  13133  hashtpg  13267  swrdnd2  13433  tgldimor  25397  outpasch  25647  xrdifh  29542  eliccioo  29639  orngsqr  29804  elzdif0  30024  qqhval2lem  30025  dfso2  31644  dfon2lem5  31692  dfon2lem6  31693  nofv  31810  nosepon  31818  ecase13d  32307  elicc3  32311  wl-exeq  33321  dvasin  33496  4atlem3a  34883  4atlem3b  34884  frege133d  38057  or3or  38319  3ornot23VD  39082  xrssre  39564