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

Theorem 3orass 1057
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 1055 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
2 orass 545 . 2 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2bitri 264 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 382  w3o 1053
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 197  df-or 384  df-3or 1055
This theorem is referenced by:  3orel1  1058  3orrot  1061  3orcoma  1063  3orcombOLD  1066  3mix1  1250  ecase23d  1476  3bior1fd  1478  cador  1587  moeq3  3416  sotric  5090  sotrieq  5091  isso2i  5096  ordzsl  7087  soxp  7335  wemapsolem  8496  rankxpsuc  8783  tcrank  8785  cardlim  8836  cardaleph  8950  grur1  9680  elnnz  11425  elznn0  11430  elznn  11431  elxr  11988  xrrebnd  12037  xaddf  12093  xrinfmss  12178  elfzlmr  12622  ssnn0fi  12824  hashv01gt1  13173  hashtpg  13305  swrdnd2  13479  tgldimor  25442  outpasch  25692  xrdifh  29670  eliccioo  29767  orngsqr  29932  elzdif0  30152  qqhval2lem  30153  dfso2  31770  dfon2lem5  31816  dfon2lem6  31817  nofv  31935  nosepon  31943  ecase13d  32432  elicc3  32436  wl-exeq  33451  dvasin  33626  4atlem3a  35201  4atlem3b  35202  frege133d  38374  or3or  38636  3ornot23VD  39396  xrssre  39877
  Copyright terms: Public domain W3C validator