mtbii Show Code edit
# An inference from a biconditional, similar to modus tollens.
## Modus Tollens
thm (mtbii () (mtbii.min (-. ps) mtbii.maj (-> ph (<-> ps ch))) (-> ph (-. ch)) mtbii.min mtbii.maj biimprd mtoi)
(-> ph (-. ch))
edit