Theorem andnand1

Description: Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011)

	Ref	Expression
Assertion	andnand1	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ⊼ ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3anass	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) )
2		pm4.63	⊢ ( ¬ ( 𝜓 → ¬ 𝜒 ) ↔ ( 𝜓 ∧ 𝜒 ) )
3	2	anbi2i	⊢ ( ( 𝜑 ∧ ¬ ( 𝜓 → ¬ 𝜒 ) ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) )
4		annim	⊢ ( ( 𝜑 ∧ ¬ ( 𝜓 → ¬ 𝜒 ) ) ↔ ¬ ( 𝜑 → ( 𝜓 → ¬ 𝜒 ) ) )
5	1 3 4	3bitr2i	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ¬ ( 𝜑 → ( 𝜓 → ¬ 𝜒 ) ) )
6		df-3nand	⊢ ( ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → ¬ 𝜒 ) ) )
7	6	notbii	⊢ ( ¬ ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ↔ ¬ ( 𝜑 → ( 𝜓 → ¬ 𝜒 ) ) )
8		nannot	⊢ ( ¬ ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ↔ ( ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ⊼ ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ) )
9	5 7 8	3bitr2i	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ⊼ ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ) )