Definition df-3nand 32395

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.)

Assertion

Ref	Expression
df-3nand	|- ( ( ph -/\ ps -/\ ch ) <-> ( ph -> ( ps -> -. ch ) ) )

Detailed syntax breakdown of Definition df-3nand

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

This definition is referenced by:  df3nandALT1  32396  df3nandALT2  32397  andnand1  32398