mpbidi Show Code edit
# A deduction from a biconditional, related to modus ponens.
## Modus Ponens
thm (mpbidi () (mpbidi.min (-> th (-> ph ps)) mpbidi.maj (-> ph (<-> ps ch))) (-> th (-> ph ch)) mpbidi.min mpbidi.maj pm5.74i sylib)
(-> th (-> ph ch))
edit