Description: Given falsum F. , we can define the negation of a wff ph as the statement that F. follows from assuming ph . (Contributed by Mario Carneiro, 9-Feb-2017) (Proof shortened by Wolf Lammen, 21-Jul-2019)