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