Theorem 3ianor 1136

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

Step	Hyp	Ref	Expression
1		ianor 1009	. . 3 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
2	1	orbi1i 942	. 2 ⊢ ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
3		ianor 1009	. . 3 ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒))
4		df-3an 1113	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	3, 4	xchnxbir 325	. 2 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒))
6		df-3or 1112	. 2 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
7	2, 5, 6	3bitr4i 295	1 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 386   ∨ wo 878   ∨ w3o 1110   ∧ w3a 1111

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 387  df-or 879  df-3or 1112  df-3an 1113

This theorem is referenced by:  3anor  1137  tppreqb  4554  fr3nr  7240  bropopvvv  7519  prinfzo0  12802  elfznelfzo  12868  ssnn0fi  13079  hashtpg  13556  swrdnd0  13722  pfxnd0  13767  lcmfunsnlem2lem2  15725  prm23ge5  15891  2irrexpq  24875  lpni  27879  xrdifh  30078  dvasin  34032  limcicciooub  40657  2zrngnring  42792