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