intnand Show Code edit
## Introduce conjunction inside contradiction
thm (intnand () (intnand.1 (-> ph (-. ps))) (-> ph (-. (/\ ch ps))) intnand.1 ch ps pm3.27 nsyl)
(-> ph (-. (/\ ch ps)))
edit