 In a lecture in 1923, Brouwer presented a proof of \(\neg \neg \neg A \leftrightarrow \neg A\) (Brouwer 1925E: 253 [Mancosu 1998:  291]).[8]  This equivalence is the one theorem in propositional logic that Brouwer ever published. The argument begins by pointing out that \(A \rightarrow B\) implies that \(\neg B \rightarrow \neg A\) (because \(\neg B\) is \(B \rightarrow \bot\) and the two implications can be composed because the consequent of the one is the antecedent of the other). It would not have been possible for Brouwer to make this inference if at the time it would have been among his proof conditions of an implication to have a proof of the antecedent, as then a proof of \(A \rightarrow B\) would lead to a proof of \(B\) and thereby make it impossible to begin establishing the second implication by proving its antecedent \(\neg B\).