- If you can prove
phi
and~ phi
, then you can proveFalse
(remember,~ phi := phi -> False
) - If you can prove
False
, then you can prove anything, including your goal at that point
So absurd phi
applies False
elimination, and have you prove False
by means of proving both phi
and ~ phi
.