impi Show Code edit
## Importation Inference
thm (impi () (1 (-> ph (-> ps ch))) (-> (-. (-> ph (-. ps))) ch)
1 ph ps ch impt ax-mp)
(-> (-. (-> ph (-. ps))) ch)
edit