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  1640  moeq3  3669  sotric  5588  sotrieq  5589  isso2i  5595  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  38411  wl-exeq  38467  dvasin  38623  4atlem3a  40655  4atlem3b  40656  frege133d  44765  or3or  45023  3ornot23VD  45829  xrssre  46360  usgrexmpl2nb0  49129  usgrexmpl2nb2  49131  usgrexmpl2nb3  49132  usgrexmpl2nb5  49134