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 ⊢φ⊼ψ⊼χ↔φ⊼ψ⊼χ⊼ψ⊼χ