Theorem cadifp

The value of the carry is, if the input carry is true, the disjunction, and if the input carry is false, the conjunction, of the other two inputs. (Contributed by BJ, 8-Oct-2019.)

Conclusion
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \operatorname{if} ( \chi , \varphi \vee \psi , \varphi \wedge \psi ) \)
Proof
l0
cad1
cad0
casesifp l0 _