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