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

Theorem 3orass 1083
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 1081 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
2 orass 916 . 2 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2bitri 276 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator