andnand1

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

		Ref	Expression
	Assertion	andnand1	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ ⊼ ψ ⊼ χ) ⊼ (φ ⊼ ψ ⊼ χ))$

Step	Hyp	Ref	Expression
1		3anass	$⊢ (φ \land ψ \land χ) \leftrightarrow (φ \land (ψ \land χ))$
2		pm4.63	$⊢ \neg (ψ \to \neg χ) \leftrightarrow (ψ \land χ)$
3	2	anbi2i	$⊢ (φ \land \neg (ψ \to \neg χ)) \leftrightarrow (φ \land (ψ \land χ))$
4		annim	$⊢ (φ \land \neg (ψ \to \neg χ)) \leftrightarrow \neg (φ \to (ψ \to \neg χ))$
5	1 3 4	3bitr2i	$⊢ (φ \land ψ \land χ) \leftrightarrow \neg (φ \to (ψ \to \neg χ))$
6		df-3nand	$⊢ (φ ⊼ ψ ⊼ χ) \leftrightarrow (φ \to (ψ \to \neg χ))$
7	6	notbii	$⊢ \neg (φ ⊼ ψ ⊼ χ) \leftrightarrow \neg (φ \to (ψ \to \neg χ))$
8		nannot	$⊢ \neg (φ ⊼ ψ ⊼ χ) \leftrightarrow ((φ ⊼ ψ ⊼ χ) ⊼ (φ ⊼ ψ ⊼ χ))$
9	5 7 8	3bitr2i	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ ⊼ ψ ⊼ χ) ⊼ (φ ⊼ ψ ⊼ χ))$

Metamath Proof Explorer