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