Theorem 3orass 1105

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 860   ∨ w3o 1101

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 861  df-3or 1103

This theorem is used by:  3orel1  1106  3orrot  1107  3orcoma  1108  3mix1  1348  ecase13d  1501  ecase23d  1502  3bior1fd  1505  cador  1637  moeq3  3674  sotric  5598  sotrieq  5599  isso2i  5605  ordzsl  7839  soxp  8123  frxp3  8145  wemapsolem  9510  rankxpsuc  9852  tcrank  9854  cardlim  9965  cardaleph  10080  grur1  10811  elnnz  12607  elznn0  12612  elznn  12613  elxr  13147  xrrebnd  13200  xaddf  13256  xrinfmss  13342  elfzlmr  13818  ssnn0fi  14028  hashv01gt1  14388  hashtpg  14529  swrdnd2  14700  pfxnd0  14733  chnccat  18688  orngsqr  20980  nofv  27832  nosepon  27840  elzs2  28603  elnnzs  28605  elznns  28606  tgldimor  28782  outpasch  29048  elplng  29073  lnincplng  29077  plngcplem  29078  plngrotlem2  29081  plngmiropp  29087  xrdifh  33136  eliccioo  33261  elzdif0  34379  qqhval2lem  34380  dfso2  36255  dfon2lem5  36285  dfon2lem6  36286  elicc3  36856  wl-df4-3mintru2  38161  wl-exeq  38217  dvasin  38383  4atlem3a  40399  4atlem3b  40400  frege133d  44519  or3or  44777  3ornot23VD  45583  xrssre  46092  usgrexmpl2nb0  48824  usgrexmpl2nb2  48826  usgrexmpl2nb3  48827  usgrexmpl2nb5  48829