mtbid Show Code edit
# A deduction from a biconditional, similar to modus tollens.
## Modus Tollens
thm (mtbid () (mtbid.min (-> ph (-. ps)) mtbid.maj (-> ph (<-> ps ch))) (-> ph (-. ch)) mtbid.min mtbid.maj biimprd mtod)
(-> ph (-. ch))
edit