pm2.43 Show Code edit
## Absorb redundant antecedent
##
## Absorption of redundant antecedent. Also called the "Contraction" or
## "Hilbert" axiom.
##
thm (pm2.43 () () (-> (-> ph (-> ph ps)) (-> ph ps))
ph ph ps ax-2 com12 hid)
(-> (-> ph (-> ph ps)) (-> ph ps))
edit