Metamath Proof Explorer

Theorem df3nandALT1

Description: The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011)

Ref Expression
Assertion df3nandALT1 ⊢ φ ⊼ ψ ⊼ χ ↔ φ ⊼ ψ ⊼ χ ⊼ ψ ⊼ χ

Proof

Step Hyp Ref Expression
1 iman ⊢ φ → ψ ⊼ χ ∧ ψ ⊼ χ ↔ ¬ φ ∧ ¬ ψ ⊼ χ ∧ ψ ⊼ χ
2 imnan ⊢ ψ → ¬ χ ↔ ¬ ψ ∧ χ
3 2 biimpi ⊢ ψ → ¬ χ → ¬ ψ ∧ χ
4 3 3 jca ⊢ ψ → ¬ χ → ¬ ψ ∧ χ ∧ ¬ ψ ∧ χ
5 2 biimpri ⊢ ¬ ψ ∧ χ → ψ → ¬ χ
6 5 adantl ⊢ ¬ ψ ∧ χ ∧ ¬ ψ ∧ χ → ψ → ¬ χ
7 4 6 impbii ⊢ ψ → ¬ χ ↔ ¬ ψ ∧ χ ∧ ¬ ψ ∧ χ
8 df-nan ⊢ ψ ⊼ χ ↔ ¬ ψ ∧ χ
9 8 8 anbi12i ⊢ ψ ⊼ χ ∧ ψ ⊼ χ ↔ ¬ ψ ∧ χ ∧ ¬ ψ ∧ χ
10 7 9 bitr4i ⊢ ψ → ¬ χ ↔ ψ ⊼ χ ∧ ψ ⊼ χ
11 10 imbi2i ⊢ φ → ψ → ¬ χ ↔ φ → ψ ⊼ χ ∧ ψ ⊼ χ
12 df-nan ⊢ ψ ⊼ χ ⊼ ψ ⊼ χ ↔ ¬ ψ ⊼ χ ∧ ψ ⊼ χ
13 12 anbi2i ⊢ φ ∧ ψ ⊼ χ ⊼ ψ ⊼ χ ↔ φ ∧ ¬ ψ ⊼ χ ∧ ψ ⊼ χ
14 13 notbii ⊢ ¬ φ ∧ ψ ⊼ χ ⊼ ψ ⊼ χ ↔ ¬ φ ∧ ¬ ψ ⊼ χ ∧ ψ ⊼ χ
15 1 11 14 3bitr4i ⊢ φ → ψ → ¬ χ ↔ ¬ φ ∧ ψ ⊼ χ ⊼ ψ ⊼ χ
16 df-3nand ⊢ φ ⊼ ψ ⊼ χ ↔ φ → ψ → ¬ χ
17 df-nan ⊢ φ ⊼ ψ ⊼ χ ⊼ ψ ⊼ χ ↔ ¬ φ ∧ ψ ⊼ χ ⊼ ψ ⊼ χ
18 15 16 17 3bitr4i ⊢ φ ⊼ ψ ⊼ χ ↔ φ ⊼ ψ ⊼ χ ⊼ ψ ⊼ χ