mpi Show Code edit
## Modus Ponens Inference
thm (mpi () (1 ps 2 (-> ph (-> ps ch))) (-> ph ch)
1 2 com12 ax-mp)
(-> ph ch)
edit