Theorem 3ianor 1124

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.) Shorten with xchnxbir 336. (Revised by Wolf Lammen, 8-Apr-2022.)

Assertion

Ref	Expression
3ianor	⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))

Proof of Theorem 3ianor

Step	Hyp	Ref	Expression
1		ianor 997	. . 3 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
2	1	orbi1i 927	. 2 ⊢ ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
3		ianor 997	. . 3 ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒))
4		df-3an 1105	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	3, 4	xchnxbir 336	. 2 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒))
6		df-3or 1104	. 2 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
7	2, 5, 6	3bitr4i 306	1 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105

This theorem is used by:  3anor  1125  tppreqb  4775  otthne  5470  fr3nr  7778  bropopvvv  8092  prinfzo0  13749  elfznelfzo  13824  ssnn0fi  14044  hashtpg  14545  hash3tpde  14553  swrdnd0  14722  pfxnd0  14753  lcmfunsnlem2lem2  16724  prm23ge5  16902  2irrexpq  26952  lpni  30908  xrdifh  33200  dvasin  38417  dflim5  44134  limcicciooub  46429  2zrngnring  49100