mpancom Show Code edit
# An inference based on modus ponens with commutation of antecedents.
## Modus Ponens & Commute
thm (mpancom () (mpancom.1 (-> ps ph) mpancom.2 (-> (/\ ph ps) ch)) (-> ps ch) mpancom.1 mpancom.2 ancoms mpdan)
(-> ps ch)
edit