Metamath Proof Explorer

Theorem df3nandALT2

Description: The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011)

Ref Expression
Assertion df3nandALT2 ⊢ φ ⊼ ψ ⊼ χ ↔ ¬ φ ∧ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 df-3nand ⊢ φ ⊼ ψ ⊼ χ ↔ φ → ψ → ¬ χ
2 imnan ⊢ ψ → ¬ χ ↔ ¬ ψ ∧ χ
3 2 imbi2i ⊢ φ → ψ → ¬ χ ↔ φ → ¬ ψ ∧ χ
4 imnan ⊢ φ → ¬ ψ ∧ χ ↔ ¬ φ ∧ ψ ∧ χ
5 3anass ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
6 4 5 xchbinxr ⊢ φ → ¬ ψ ∧ χ ↔ ¬ φ ∧ ψ ∧ χ
7 1 3 6 3bitri ⊢ φ ⊼ ψ ⊼ χ ↔ ¬ φ ∧ ψ ∧ χ