Metamath Proof Explorer

Theorem andnand1

Description: Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011)

Ref Expression
Assertion andnand1 ⊢ φ ∧ ψ ∧ χ ↔ φ ⊼ ψ ⊼ χ ⊼ φ ⊼ ψ ⊼ χ

Proof

Step Hyp Ref Expression
1 3anass ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
2 pm4.63 ⊢ ¬ ψ → ¬ χ ↔ ψ ∧ χ
3 2 anbi2i ⊢ φ ∧ ¬ ψ → ¬ χ ↔ φ ∧ ψ ∧ χ
4 annim ⊢ φ ∧ ¬ ψ → ¬ χ ↔ ¬ φ → ψ → ¬ χ
5 1 3 4 3bitr2i ⊢ φ ∧ ψ ∧ χ ↔ ¬ φ → ψ → ¬ χ
6 df-3nand ⊢ φ ⊼ ψ ⊼ χ ↔ φ → ψ → ¬ χ
7 6 notbii ⊢ ¬ φ ⊼ ψ ⊼ χ ↔ ¬ φ → ψ → ¬ χ
8 nannot ⊢ ¬ φ ⊼ ψ ⊼ χ ↔ φ ⊼ ψ ⊼ χ ⊼ φ ⊼ ψ ⊼ χ
9 5 7 8 3bitr2i ⊢ φ ∧ ψ ∧ χ ↔ φ ⊼ ψ ⊼ χ ⊼ φ ⊼ ψ ⊼ χ