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

Theorem 3ianor 1108
Description: Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Revised by Wolf Lammen, 8-Apr-2022.)
Assertion
Ref Expression
3ianor (¬ (𝜑𝜓𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))

Proof of Theorem 3ianor
StepHypRef Expression
1 ianor 981 . . 3 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
21orbi1i 913 . 2 ((¬ (𝜑𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
3 ianor 981 . . 3 (¬ ((𝜑𝜓) ∧ 𝜒) ↔ (¬ (𝜑𝜓) ∨ ¬ 𝜒))
4 df-3an 1090 . . 3 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
53, 4xchnxbir 333 . 2 (¬ (𝜑𝜓𝜒) ↔ (¬ (𝜑𝜓) ∨ ¬ 𝜒))
6 df-3or 1089 . 2 ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
72, 5, 63bitr4i 303 1 (¬ (𝜑𝜓𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 397  wo 846  w3o 1087  w3a 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 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090
This theorem is referenced by:  3anor  1109  tppreqb  4809  otthne  5487  fr3nr  7759  bropopvvv  8076  prinfzo0  13671  elfznelfzo  13737  ssnn0fi  13950  hashtpg  14446  swrdnd0  14607  pfxnd0  14638  lcmfunsnlem2lem2  16576  prm23ge5  16748  2irrexpq  26239  lpni  29764  xrdifh  32022  dvasin  36620  dflim5  42127  limcicciooub  44401  2zrngnring  46898
  Copyright terms: Public domain W3C validator