claim !P:prop.!Q:prop.P & Q -> P