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

Theorem 3ianor 1107
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 980 . . 3 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
21orbi1i 912 . 2 ((¬ (𝜑𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
3 ianor 980 . . 3 (¬ ((𝜑𝜓) ∧ 𝜒) ↔ (¬ (𝜑𝜓) ∨ ¬ 𝜒))
4 df-3an 1089 . . 3 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
53, 4xchnxbir 332 . 2 (¬ (𝜑𝜓𝜒) ↔ (¬ (𝜑𝜓) ∨ ¬ 𝜒))
6 df-3or 1088 . 2 ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
72, 5, 63bitr4i 302 1 (¬ (𝜑𝜓𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 396  wo 845  w3o 1086  w3a 1087
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 397  df-or 846  df-3or 1088  df-3an 1089
This theorem is referenced by:  3anor  1108  tppreqb  4808  otthne  5486  fr3nr  7758  bropopvvv  8075  prinfzo0  13670  elfznelfzo  13736  ssnn0fi  13949  hashtpg  14445  swrdnd0  14606  pfxnd0  14637  lcmfunsnlem2lem2  16575  prm23ge5  16747  2irrexpq  26237  lpni  29728  xrdifh  31986  dvasin  36567  dflim5  42069  limcicciooub  44343  2zrngnring  46840
  Copyright terms: Public domain W3C validator