MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3orass Structured version   Visualization version   GIF version

Theorem 3orass 1087
Description: Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3orass ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))

Proof of Theorem 3orass
StepHypRef Expression
1 df-3or 1085 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
2 orass 919 . 2 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2bitri 278 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wo 844  w3o 1083
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 845  df-3or 1085
This theorem is referenced by:  3orel1  1088  3orrot  1089  3orcoma  1090  3mix1  1327  ecase23d  1470  3bior1fd  1472  cador  1610  moeq3  3654  sotric  5469  sotrieq  5470  isso2i  5476  ordzsl  7544  soxp  7810  wemapsolem  9002  rankxpsuc  9299  tcrank  9301  cardlim  9389  cardaleph  9504  grur1  10235  elnnz  11983  elznn0  11988  elznn  11989  elxr  12503  xrrebnd  12553  xaddf  12609  xrinfmss  12695  elfzlmr  13150  ssnn0fi  13352  hashv01gt1  13705  hashtpg  13843  swrdnd2  14012  pfxnd0  14045  tgldimor  26299  outpasch  26552  xrdifh  30532  eliccioo  30636  orngsqr  30931  elzdif0  31329  qqhval2lem  31330  dfso2  33098  dfon2lem5  33140  dfon2lem6  33141  nofv  33272  nosepon  33280  ecase13d  33769  elicc3  33773  wl-df4-3mintru2  34897  wl-exeq  34932  dvasin  35134  4atlem3a  36886  4atlem3b  36887  frege133d  40453  or3or  40711  3ornot23VD  41540  xrssre  41967
  Copyright terms: Public domain W3C validator