Theorem 3orass 1092

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

Syntax hints:   ↔ wb 209   ∨ wo 847   ∨ w3o 1088

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 210  df-or 848  df-3or 1090

This theorem is referenced by:  3orel1  1093  3orrot  1094  3orcoma  1095  3mix1  1332  ecase23d  1475  3bior1fd  1477  cador  1615  moeq3  3614  sotric  5481  sotrieq  5482  isso2i  5488  ordzsl  7602  soxp  7874  wemapsolem  9144  rankxpsuc  9463  tcrank  9465  cardlim  9553  cardaleph  9668  grur1  10399  elnnz  12151  elznn0  12156  elznn  12157  elxr  12673  xrrebnd  12723  xaddf  12779  xrinfmss  12865  elfzlmr  13321  ssnn0fi  13523  hashv01gt1  13876  hashtpg  14016  swrdnd2  14185  pfxnd0  14218  tgldimor  26547  outpasch  26800  xrdifh  30775  eliccioo  30879  orngsqr  31176  elzdif0  31596  qqhval2lem  31597  dfso2  33391  dfon2lem5  33433  dfon2lem6  33434  frxp3  33477  nofv  33546  nosepon  33554  ecase13d  34188  elicc3  34192  wl-df4-3mintru2  35344  wl-exeq  35379  dvasin  35547  4atlem3a  37297  4atlem3b  37298  frege133d  40991  or3or  41249  3ornot23VD  42081  xrssre  42501