Definition df-3nand

Description: The double nand. This definition allows us to express the input of three variables only being false if all three are true. (Contributed by Anthony Hart, 2-Sep-2011)

	Ref	Expression
Assertion	df-3nand	$$⊢\left(\phi ⊼\psi ⊼\chi \right)\leftrightarrow \left(\phi \to \left(\psi \to \neg \chi \right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2		wch	$$wff\chi$$
3	0 1 2	w3nand	$$wff\left(\phi ⊼\psi ⊼\chi \right)$$
4	2	wn	$$wff\neg \chi$$
5	1 4	wi	$$wff\left(\psi \to \neg \chi \right)$$
6	0 5	wi	$$wff\left(\phi \to \left(\psi \to \neg \chi \right)\right)$$
7	3 6	wb	$$wff\left(\left(\phi ⊼\psi ⊼\chi \right)\leftrightarrow \left(\phi \to \left(\psi \to \neg \chi \right)\right)\right)$$