A formula is equivalent to its negation implying it. Theorem *4.81 of [WhiteheadRussell] p. 122. Note that the second step, using pm2.24, could also use [ax-1]. (Contributed by NM, 3-Jan-2005.)
A formula is equivalent to its negation implying it. Theorem *4.81 of [WhiteheadRussell] p. 122. Note that the second step, using pm2.24, could also use [ax-1]. (Contributed by NM, 3-Jan-2005.)