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