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