mtbir Show Code edit
## Modus Tollens
##
## [ [ (-. [ ps)
## (<-> [ ph ] [ [ ps)
## (-. [ ph) ] ] ]
##
thm (mtbir () (1 (-. ps) 2 (<-> ph ps)) (-. ph)
1 2 notbii mpbir)
(-. ph)
edit