mpbii Show Code edit
## Modus Ponens
##
## [ ps ]
## (-> ph (<-> [ ps ] ch))
## (-> ph [ [ ch))
##
thm (mpbii () (1 ps 2 (-> ph (<-> ps ch))) (-> ph ch)
1 2 biimpd mpi)
(-> ph ch)
edit