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

Theorem 3ianor 1133
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 1005 . . 3 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
21orbi1i 938 . 2 ((¬ (𝜑𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
3 ianor 1005 . . 3 (¬ ((𝜑𝜓) ∧ 𝜒) ↔ (¬ (𝜑𝜓) ∨ ¬ 𝜒))
4 df-3an 1110 . . 3 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
53, 4xchnxbir 325 . 2 (¬ (𝜑𝜓𝜒) ↔ (¬ (𝜑𝜓) ∨ ¬ 𝜒))
6 df-3or 1109 . 2 ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
72, 5, 63bitr4i 295 1 (¬ (𝜑𝜓𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198  wa 385  wo 874  w3o 1107  w3a 1108
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 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110
This theorem is referenced by:  3anor  1134  tppreqb  4524  fr3nr  7213  bropopvvv  7492  prinfzo0  12762  elfznelfzo  12828  ssnn0fi  13039  hashtpg  13516  swrdnd0  13686  pfxnd0  13731  lcmfunsnlem2lem2  15687  prm23ge5  15853  2irrexpq  24817  lpni  27860  xrdifh  30060  dvasin  33984  limcicciooub  40613  2zrngnring  42751
  Copyright terms: Public domain W3C validator