df-nand Show Code edit
defthm (df-nand wff (-/\ ph ps) () () (<-> (-/\ ph ps) (-. (/\ ph ps)))
(-. (/\ ph ps)) biid)
(<-> (-. (/\ ph ps)) (-. (/\ ph ps)))
edit