Definition df-3nand 33746

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	⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 → (𝜓 → ¬ 𝜒)))

Detailed syntax breakdown of Definition df-3nand

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 2, 3	w3nand 33745	. 2 wff (𝜑 ⊼ 𝜓 ⊼ 𝜒)
5	3	wn 3	. . . 4 wff ¬ 𝜒
6	2, 5	wi 4	. . 3 wff (𝜓 → ¬ 𝜒)
7	1, 6	wi 4	. 2 wff (𝜑 → (𝜓 → ¬ 𝜒))
8	4, 7	wb 208	1 wff ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 → (𝜓 → ¬ 𝜒)))

This definition is referenced by:  df3nandALT1  33747  df3nandALT2  33748  andnand1  33749