Theorem 3orass 1088

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 1086	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 920	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 205   ∨ wo 846   ∨ w3o 1084

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 206  df-or 847  df-3or 1086

This theorem is referenced by:  3orel1  1089  3orrot  1090  3orcoma  1091  3mix1  1328  ecase23d  1470  3bior1fd  1472  cador  1602  moeq3  3707  sotric  5618  sotrieq  5619  isso2i  5625  ordzsl  7849  soxp  8134  frxp3  8156  wemapsolem  9574  rankxpsuc  9906  tcrank  9908  cardlim  9996  cardaleph  10113  grur1  10844  elnnz  12599  elznn0  12604  elznn  12605  elxr  13129  xrrebnd  13180  xaddf  13236  xrinfmss  13322  elfzlmr  13779  ssnn0fi  13983  hashv01gt1  14337  hashtpg  14479  swrdnd2  14638  pfxnd0  14671  nofv  27603  nosepon  27611  tgldimor  28319  outpasch  28572  xrdifh  32561  eliccioo  32667  orngsqr  33032  elzdif0  33581  qqhval2lem  33582  dfso2  35349  dfon2lem5  35383  dfon2lem6  35384  ecase13d  35797  elicc3  35801  wl-df4-3mintru2  36966  wl-exeq  37001  dvasin  37177  4atlem3a  39070  4atlem3b  39071  frege133d  43195  or3or  43453  3ornot23VD  44286  xrssre  44730