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

Step	Hyp	Ref	Expression
1		3anor 1047	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
2	1	con2bii 346	. 2 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒))
3	2	bicomi 213	1 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))

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