mpan9 Show Code edit
# Modus ponens conjoining dissimilar antecedents.
## Modus Ponens
thm (mpan9 () (mpan9.1 (-> ph ps) mpan9.2 (-> ch (-> ps th))) (-> (/\ ph ch) th) mpan9.1 ch adantr mpan9.2 ph adantl mpd)
(-> (/\ ph ch) th)
edit