Theorem hadifp

The value of the adder sum is, if the first input is true, the biconditionality, and if the first input is false, the exclusive disjunction, of the other two inputs. (Contributed by BJ, 11-Aug-2020.)

Conclusion
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \operatorname{if} ( \varphi , \psi \leftrightarrow \chi , \psi \veebar \chi ) \)
Proof
had1
l1
biimpi _
had0
biimpi _
casesifp l1 _