mpbiri Show Code edit
## Modus Ponens
thm (mpbiri () (1 ch 2 (-> ph (<-> ps ch))) (-> ph ps)
1 2 biimprd mpi)
(-> ph ps)
edit