intnanr Show Code edit
## Introduce conjunction inside contradiction
thm (intnanr () (intnan.1 (-. ph)) (-. (/\ ph ps)) intnan.1 ph ps pm3.26 mto)
(-. (/\ ph ps))
edit