mt2bi Show Code edit
# A false consequent falsifies an antecedent.
## Modus Tollens
thm (mt2bi () (mt2bi.1 ph) (<-> (-. ps) (-> ps (-. ph))) ps (-. ph) pm2.21 mt2bi.1 ps ph con2 mpi impbii)
(<-> (-. ps) (-> ps (-. ph)))
edit