mtt Show Code edit
# Modus-tollens-like theorem.
## Modus Tollens
thm (mtt () () (-> (-. ph) (<-> (-. ps) (-> ps ph))) ps ph pm2.21 ps ph con3 com12 impbid2)
(-> (-. ph) (<-> (-. ps) (-> ps ph)))
edit