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  5531  sotrieq  5532  isso2i  5538  ordzsl  7692  soxp  7970  wemapsolem  9309  rankxpsuc  9640  tcrank  9642  cardlim  9730  cardaleph  9845  grur1  10576  elnnz  12329  elznn0  12334  elznn  12335  elxr  12852  xrrebnd  12902  xaddf  12958  xrinfmss  13044  elfzlmr  13501  ssnn0fi  13705  hashv01gt1  14059  hashtpg  14199  swrdnd2  14368  pfxnd0  14401  tgldimor  26863  outpasch  27116  xrdifh  31101  eliccioo  31205  orngsqr  31503  elzdif0  31930  qqhval2lem  31931  dfso2  33722  dfon2lem5  33763  dfon2lem6  33764  frxp3  33797  nofv  33860  nosepon  33868  ecase13d  34502  elicc3  34506  wl-df4-3mintru2  35658  wl-exeq  35693  dvasin  35861  4atlem3a  37611  4atlem3b  37612  frege133d  41373  or3or  41631  3ornot23VD  42467  xrssre  42887