Theorem 3ianor 1107

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 982	. . 3 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
2	1	orbi1i 912	. 2 ⊢ ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
3		ianor 982	. . 3 ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒))
4		df-3an 1089	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	3, 4	xchnxbir 333	. 2 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒))
6		df-3or 1088	. 2 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒))
7	2, 5, 6	3bitr4i 303	1 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∨ w3o 1086   ∧ w3a 1087

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 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089

This theorem is referenced by:  3anor  1108  tppreqb  4830  otthne  5506  fr3nr  7807  bropopvvv  8131  prinfzo0  13755  elfznelfzo  13822  ssnn0fi  14036  hashtpg  14534  hash3tpde  14542  swrdnd0  14705  pfxnd0  14736  lcmfunsnlem2lem2  16686  prm23ge5  16862  2irrexpq  26791  lpni  30512  xrdifh  32785  dvasin  37664  dflim5  43291  limcicciooub  45558  2zrngnring  47981