Theorem 3orass 1106

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 1104	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 935	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  3orel1  1107  3orrot  1108  3orcoma  1109  3mix1  1349  ecase13d  1502  ecase23d  1503  3bior1fd  1506  cador  1641  moeq3  3670  sotric  5589  sotrieq  5590  isso2i  5596  ordzsl  7856  soxp  8141  frxp3  8168  wemapsolem  9544  rankxpsuc  9899  tcrank  9901  cardlim  10053  cardaleph  10168  grur1  10905  elnnz  12703  elznn0  12708  elznn  12709  elxr  13245  xrrebnd  13298  xaddf  13354  xrinfmss  13440  elfzlmr  13917  ssnn0fi  14128  hashv01gt1  14489  hashtpg  14630  swrdnd2  14805  pfxnd0  14838  chnccat  18800  orngsqr  21123  nofv  28014  nosepon  28022  elzs2  28785  elnnzs  28787  elznns  28788  tgldimor  28965  outpasch  29233  elplng  29258  lnincplng  29262  plngcplem  29263  plngrotlem2  29266  plngmiropp  29272  xrdifh  33372  eliccioo  33497  elzdif0  34612  qqhval2lem  34613  dfso2  36520  dfon2lem5  36549  dfon2lem6  36550  elicc3  37105  wl-df4-3mintru2  38410  wl-exeq  38466  dvasin  38622  4atlem3a  40654  4atlem3b  40655  frege133d  44764  or3or  45022  3ornot23VD  45828  xrssre  46359  usgrexmpl2nb0  49128  usgrexmpl2nb2  49130  usgrexmpl2nb3  49131  usgrexmpl2nb5  49133