Theorem 3orass 1102

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

Syntax hints:   ↔ wb 208   ∨ wo 858   ∨ w3o 1098

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 859  df-3or 1100

This theorem is referenced by:  3orel1  1103  3orrot  1104  3orcoma  1105  3mix1  1345  ecase23d  1496  3bior1fd  1498  cador  1630  moeq3  3677  sotric  5587  sotrieq  5588  isso2i  5594  ordzsl  7827  soxp  8111  frxp3  8133  wemapsolem  9500  rankxpsuc  9842  tcrank  9844  cardlim  9932  cardaleph  10047  grur1  10780  elnnz  12580  elznn0  12585  elznn  12586  elxr  13120  xrrebnd  13173  xaddf  13229  xrinfmss  13315  elfzlmr  13790  ssnn0fi  14000  hashv01gt1  14360  hashtpg  14500  swrdnd2  14671  pfxnd0  14704  chnccat  18660  orngsqr  20917  nofv  27723  nosepon  27731  elzs2  28494  elnnzs  28496  elznns  28497  tgldimor  28673  outpasch  28930  elplng  28989  lnincplng  28993  plngcplem  28994  plngrotlem2  28997  xrdifh  32984  eliccioo  33110  elzdif0  34279  qqhval2lem  34280  dfso2  36110  dfon2lem5  36140  dfon2lem6  36141  ecase13d  36678  elicc3  36682  wl-df4-3mintru2  37986  wl-exeq  38042  dvasin  38208  4atlem3a  40226  4atlem3b  40227  frege133d  44346  or3or  44604  3ornot23VD  45427  xrssre  45929  usgrexmpl2nb0  48658  usgrexmpl2nb2  48660  usgrexmpl2nb3  48661  usgrexmpl2nb5  48663