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	|- ( ( ph -/\ ps -/\ ch ) <-> ( ph -> ( ps -> -. ch ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2		wch	|- ch
3	0 1 2	w3nand	|- ( ph -/\ ps -/\ ch )
4	2	wn	|- -. ch
5	1 4	wi	|- ( ps -> -. ch )
6	0 5	wi	|- ( ph -> ( ps -> -. ch ) )
7	3 6	wb	|- ( ( ph -/\ ps -/\ ch ) <-> ( ph -> ( ps -> -. ch ) ) )