Theorem nanan 1289

Description: Write 'and' in terms of 'nand'. (Contributed by Mario Carneiro, 9-May-2015.)

Assertion

Ref	Expression
nanan	|- ((ph /\ ps) <-> -. (ph -/\ ps))

Proof of Theorem nanan

Step	Hyp	Ref	Expression
1		df-nan 1288	. 2 |- ((ph -/\ ps) <-> -. (ph /\ ps))
2	1	con2bii 322	1 |- ((ph /\ ps) <-> -. (ph -/\ ps))

This proof depends on syntax axioms:  -. wn 3   <-> wb 176   /\ wa 358   -/\ wnan 1287

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-nan 1288

This theorem is used by: (None)