Theorem 3orass 1096

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

Syntax hints:   ↔ wb 208   ∨ wo 854   ∨ w3o 1092

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 855  df-3or 1094

This theorem is referenced by:  3orel1  1097  3orrot  1098  3orcoma  1099  3mix1  1338  ecase23d  1482  3bior1fd  1484  cador  1616  moeq3  3655  sotric  5559  sotrieq  5560  isso2i  5566  ordzsl  7789  soxp  8073  frxp3  8095  wemapsolem  9459  rankxpsuc  9801  tcrank  9803  cardlim  9891  cardaleph  10006  grur1  10738  elnnz  12529  elznn0  12534  elznn  12535  elxr  13062  xrrebnd  13115  xaddf  13171  xrinfmss  13257  elfzlmr  13732  ssnn0fi  13942  hashv01gt1  14302  hashtpg  14442  swrdnd2  14613  pfxnd0  14646  chnccat  18587  orngsqr  20842  nofv  27643  nosepon  27651  elzs2  28413  elnnzs  28415  elznns  28416  tgldimor  28592  outpasch  28845  xrdifh  32876  eliccioo  33013  elzdif0  34176  qqhval2lem  34177  dfso2  35998  dfon2lem5  36028  dfon2lem6  36029  ecase13d  36556  elicc3  36560  wl-df4-3mintru2  37864  wl-exeq  37920  dvasin  38086  4atlem3a  40104  4atlem3b  40105  frege133d  44224  or3or  44482  3ornot23VD  45305  xrssre  45807  usgrexmpl2nb0  48536  usgrexmpl2nb2  48538  usgrexmpl2nb3  48539  usgrexmpl2nb5  48541