# Metamath Proof Explorer

## Theorem 3ianor

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)

Ref Expression
Assertion 3ianor ${⊢}¬\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left(¬{\phi }\vee ¬{\psi }\vee ¬{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 ianor ${⊢}¬\left({\phi }\wedge {\psi }\right)↔\left(¬{\phi }\vee ¬{\psi }\right)$
2 1 orbi1i ${⊢}\left(¬\left({\phi }\wedge {\psi }\right)\vee ¬{\chi }\right)↔\left(\left(¬{\phi }\vee ¬{\psi }\right)\vee ¬{\chi }\right)$
3 ianor ${⊢}¬\left(\left({\phi }\wedge {\psi }\right)\wedge {\chi }\right)↔\left(¬\left({\phi }\wedge {\psi }\right)\vee ¬{\chi }\right)$
4 df-3an ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\wedge {\chi }\right)$
5 3 4 xchnxbir ${⊢}¬\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left(¬\left({\phi }\wedge {\psi }\right)\vee ¬{\chi }\right)$
6 df-3or ${⊢}\left(¬{\phi }\vee ¬{\psi }\vee ¬{\chi }\right)↔\left(\left(¬{\phi }\vee ¬{\psi }\right)\vee ¬{\chi }\right)$
7 2 5 6 3bitr4i ${⊢}¬\left({\phi }\wedge {\psi }\wedge {\chi }\right)↔\left(¬{\phi }\vee ¬{\psi }\vee ¬{\chi }\right)$