pm2.43i Show Code edit
# a.k.a. impsimpi
## Absorb redundant antecedent
##
## (-> ph [ (-> ph ps))
## [ (-> ph ps)
##
thm (pm2.43i () (1 (-> ph (-> ph ps))) (-> ph ps)
1 a2i hid)
(-> ph ps)
edit