Theorem 3orass 1083

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 1081	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 916	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 276	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 207   ∨ wo 842   ∨ w3o 1079

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 208  df-or 843  df-3or 1081

This theorem is referenced by:  3orel1  1084  3orrot  1085  3orcoma  1086  3mix1  1323  ecase23d  1465  3bior1fd  1467  cador  1590  moeq3  3639  sotric  5389  sotrieq  5390  isso2i  5396  ordzsl  7416  soxp  7676  wemapsolem  8860  rankxpsuc  9157  tcrank  9159  cardlim  9247  cardaleph  9361  grur1  10088  elnnz  11839  elznn0  11844  elznn  11845  elxr  12361  xrrebnd  12411  xaddf  12467  xrinfmss  12553  elfzlmr  13001  ssnn0fi  13203  hashv01gt1  13555  hashtpg  13689  swrdnd2  13853  pfxnd0  13886  tgldimor  25970  outpasch  26223  xrdifh  30191  eliccioo  30291  orngsqr  30531  elzdif0  30838  qqhval2lem  30839  dfso2  32598  dfon2lem5  32640  dfon2lem6  32641  nofv  32773  nosepon  32781  ecase13d  33270  elicc3  33274  wl-exeq  34306  dvasin  34509  4atlem3a  36264  4atlem3b  36265  frege133d  39595  or3or  39856  3ornot23VD  40720  xrssre  41157