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

Theorem 3ianor 1048
 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 1047 . . 3 ((𝜑𝜓𝜒) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
21con2bii 346 . 2 ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ¬ (𝜑𝜓𝜒))
32bicomi 213 1 (¬ (𝜑𝜓𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195   ∨ w3o 1030   ∧ w3a 1031 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 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033 This theorem is referenced by:  tppreqb  4277  funtpgOLD  5857  fr3nr  6871  bropopvvv  7142  elfznelfzo  12439  ssnn0fi  12646  hashtpg  13121  lcmfunsnlem2lem2  15190  prm23ge5  15358  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  2spotdisj  26588  lpni  26722  xrdifh  28932  dvasin  32666  limcicciooub  38704  prinfzo0  40363  2zrngnring  41742
 Copyright terms: Public domain W3C validator