mp2 Show Code edit
## Double Modus Ponens
thm (mp2 () (1 ph 2 ps 3 (-> ph (-> ps ch))) ch
2 1 3 ax-mp ax-mp)
ch
edit