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