This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ↔ ( 𝜑 ⊼ ( ( 𝜓 ⊼ 𝜒 ) ⊼ ( 𝜓 ⊼ 𝜒 ) ) ) )