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

Theorem 3ianor 1054
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.)
Assertion
Ref Expression
3ianor (¬ (𝜑𝜓𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))

Proof of Theorem 3ianor
StepHypRef Expression
1 3anor 1053 . . 3 ((𝜑𝜓𝜒) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
21con2bii 347 . 2 ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ¬ (𝜑𝜓𝜒))
32bicomi 214 1 (¬ (𝜑𝜓𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  w3o 1036  w3a 1037
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 385  df-an 386  df-3or 1038  df-3an 1039
This theorem is referenced by:  tppreqb  4334  funtpgOLD  5941  fr3nr  6976  bropopvvv  7252  prinfzo0  12502  elfznelfzo  12569  ssnn0fi  12779  hashtpg  13262  lcmfunsnlem2lem2  15346  prm23ge5  15514  lpni  27316  xrdifh  29527  dvasin  33476  limcicciooub  39675  2zrngnring  41723
  Copyright terms: Public domain W3C validator