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