This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-3nand

Description: The double nand. This definition allows 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	⊢ ( ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → ¬ 𝜒 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3	0 1 2	w3nand	⊢ ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 )
4	2	wn	⊢ ¬ 𝜒
5	1 4	wi	⊢ ( 𝜓 → ¬ 𝜒 )
6	0 5	wi	⊢ ( 𝜑 → ( 𝜓 → ¬ 𝜒 ) )
7	3 6	wb	⊢ ( ( 𝜑 ⊼ 𝜓 ⊼ 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → ¬ 𝜒 ) ) )