mpbi Show Code edit
## Modus Ponens
##
## ph ] ] ]
## (<-> ph ] [ ps ] )
## [ [ ps ]
##
thm (mpbi () (1 ph 2 (<-> ph ps)) ps
1 2 biimpi ax-mp)
ps
edit