mp2an Show Code edit
## Modus Ponens
##
## ph ] ] ] ]
## [ [ ps ] ]
## (-> (/\ ph ] [ ps ] ) [ ch)
## [ [ [ [ ch
##
thm (mp2an () (mp2an.1 ph mp2an.2 ps mp2an.3 (-> (/\ ph ps) ch)) ch mp2an.2 mp2an.1 mp2an.3 mpan ax-mp)
ch
edit