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 biranri ⊢ ¬ ψ ∧ χ ∧ ¬ ψ ∧ χ → ψ → ¬ χ
6 4 5 impbii ⊢ ψ → ¬ χ ↔ ¬ ψ ∧ χ ∧ ¬ ψ ∧ χ
7 df-nan ⊢ ψ ⊼ χ ↔ ¬ ψ ∧ χ
8 7 7 anbi12i ⊢ ψ ⊼ χ ∧ ψ ⊼ χ ↔ ¬ ψ ∧ χ ∧ ¬ ψ ∧ χ
9 6 8 bitr4i ⊢ ψ → ¬ χ ↔ ψ ⊼ χ ∧ ψ ⊼ χ
10 9 imbi2i ⊢ φ → ψ → ¬ χ ↔ φ → ψ ⊼ χ ∧ ψ ⊼ χ
11 df-nan ⊢ ψ ⊼ χ ⊼ ψ ⊼ χ ↔ ¬ ψ ⊼ χ ∧ ψ ⊼ χ
12 11 anbi2i ⊢ φ ∧ ψ ⊼ χ ⊼ ψ ⊼ χ ↔ φ ∧ ¬ ψ ⊼ χ ∧ ψ ⊼ χ
13 12 notbii ⊢ ¬ φ ∧ ψ ⊼ χ ⊼ ψ ⊼ χ ↔ ¬ φ ∧ ¬ ψ ⊼ χ ∧ ψ ⊼ χ
14 1 10 13 3bitr4i ⊢ φ → ψ → ¬ χ ↔ ¬ φ ∧ ψ ⊼ χ ⊼ ψ ⊼ χ
15 df-3nand ⊢ φ ⊼ ψ ⊼ χ ↔ φ → ψ → ¬ χ
16 df-nan ⊢ φ ⊼ ψ ⊼ χ ⊼ ψ ⊼ χ ↔ ¬ φ ∧ ψ ⊼ χ ⊼ ψ ⊼ χ
17 14 15 16 3bitr4i ⊢ φ ⊼ ψ ⊼ χ ↔ φ ⊼ ψ ⊼ χ ⊼ ψ ⊼ χ