preand2i Show Code edit
## Simplification
thm (preand2i () (1 (-. (-> ph (-. ps)))) ps
1 ph ps preand2 ax-mp)
ps
edit