Theorem df3nandALT1

Description: The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011)

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

Proof

Step	Hyp	Ref	Expression
1		iman	|- ( ( ph -> ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) ) <-> -. ( ph /\ -. ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) ) )
2		imnan	|- ( ( ps -> -. ch ) <-> -. ( ps /\ ch ) )
3	2	biimpi	|- ( ( ps -> -. ch ) -> -. ( ps /\ ch ) )
4	3 3	jca	|- ( ( ps -> -. ch ) -> ( -. ( ps /\ ch ) /\ -. ( ps /\ ch ) ) )
5	2	biimpri	|- ( -. ( ps /\ ch ) -> ( ps -> -. ch ) )
6	5	adantl	|- ( ( -. ( ps /\ ch ) /\ -. ( ps /\ ch ) ) -> ( ps -> -. ch ) )
7	4 6	impbii	|- ( ( ps -> -. ch ) <-> ( -. ( ps /\ ch ) /\ -. ( ps /\ ch ) ) )
8		df-nan	|- ( ( ps -/\ ch ) <-> -. ( ps /\ ch ) )
9	8 8	anbi12i	|- ( ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) <-> ( -. ( ps /\ ch ) /\ -. ( ps /\ ch ) ) )
10	7 9	bitr4i	|- ( ( ps -> -. ch ) <-> ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) )
11	10	imbi2i	|- ( ( ph -> ( ps -> -. ch ) ) <-> ( ph -> ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) ) )
12		df-nan	|- ( ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) <-> -. ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) )
13	12	anbi2i	|- ( ( ph /\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) <-> ( ph /\ -. ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) ) )
14	13	notbii	|- ( -. ( ph /\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) <-> -. ( ph /\ -. ( ( ps -/\ ch ) /\ ( ps -/\ ch ) ) ) )
15	1 11 14	3bitr4i	|- ( ( ph -> ( ps -> -. ch ) ) <-> -. ( ph /\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) )
16		df-3nand	|- ( ( ph -/\ ps -/\ ch ) <-> ( ph -> ( ps -> -. ch ) ) )
17		df-nan	|- ( ( ph -/\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) <-> -. ( ph /\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) )
18	15 16 17	3bitr4i	|- ( ( ph -/\ ps -/\ ch ) <-> ( ph -/\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) )