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

Theorem 3ianor 1104
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 979 . . 3 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
21orbi1i 911 . 2 ((¬ (𝜑𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
3 ianor 979 . . 3 (¬ ((𝜑𝜓) ∧ 𝜒) ↔ (¬ (𝜑𝜓) ∨ ¬ 𝜒))
4 df-3an 1086 . . 3 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
53, 4xchnxbir 332 . 2 (¬ (𝜑𝜓𝜒) ↔ (¬ (𝜑𝜓) ∨ ¬ 𝜒))
6 df-3or 1085 . 2 ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
72, 5, 63bitr4i 302 1 (¬ (𝜑𝜓𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 394  wo 845  w3o 1083  w3a 1084
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 395  df-or 846  df-3or 1085  df-3an 1086
This theorem is referenced by:  3anor  1105  tppreqb  4813  otthne  5492  fr3nr  7780  bropopvvv  8101  prinfzo0  13711  elfznelfzo  13777  ssnn0fi  13990  hashtpg  14486  swrdnd0  14647  pfxnd0  14678  lcmfunsnlem2lem2  16617  prm23ge5  16791  2irrexpq  26685  lpni  30310  xrdifh  32569  dvasin  37210  dflim5  42789  limcicciooub  45054  2zrngnring  47398
  Copyright terms: Public domain W3C validator