Theorem df3nandALT2

Description: The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011)

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

Proof

Step	Hyp	Ref	Expression
1		df-3nand	⊢ ( ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → ¬ 𝜒 ) ) )
2		imnan	⊢ ( ( 𝜓 → ¬ 𝜒 ) ↔ ¬ ( 𝜓 ∧ 𝜒 ) )
3	2	imbi2i	⊢ ( ( 𝜑 → ( 𝜓 → ¬ 𝜒 ) ) ↔ ( 𝜑 → ¬ ( 𝜓 ∧ 𝜒 ) ) )
4		imnan	⊢ ( ( 𝜑 → ¬ ( 𝜓 ∧ 𝜒 ) ) ↔ ¬ ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) )
5		3anass	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) )
6	4 5	xchbinxr	⊢ ( ( 𝜑 → ¬ ( 𝜓 ∧ 𝜒 ) ) ↔ ¬ ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) )
7	1 3 6	3bitri	⊢ ( ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ↔ ¬ ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) )