Theorem df3nandALT2

Description: The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011)

	Ref	Expression
Assertion	df3nandALT2	|- ( ( ph -/\ ps -/\ ch ) <-> -. ( ph /\ ps /\ ch ) )

Proof

Step	Hyp	Ref	Expression
1		df-3nand	|- ( ( ph -/\ ps -/\ ch ) <-> ( ph -> ( ps -> -. ch ) ) )
2		imnan	|- ( ( ps -> -. ch ) <-> -. ( ps /\ ch ) )
3	2	imbi2i	|- ( ( ph -> ( ps -> -. ch ) ) <-> ( ph -> -. ( ps /\ ch ) ) )
4		imnan	|- ( ( ph -> -. ( ps /\ ch ) ) <-> -. ( ph /\ ( ps /\ ch ) ) )
5		3anass	|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
6	4 5	xchbinxr	|- ( ( ph -> -. ( ps /\ ch ) ) <-> -. ( ph /\ ps /\ ch ) )
7	1 3 6	3bitri	|- ( ( ph -/\ ps -/\ ch ) <-> -. ( ph /\ ps /\ ch ) )