Theorem cad1

If one input is true, then the adder carry is true exactly when at least one of the other two inputs is true. (Contributed by Mario Carneiro, 8-Sep-2016.) (Proof shortened by Wolf Lammen, 19-Jun-2020.)

Conclusion
\( \vdash \chi \rightarrow (\text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \vee \psi) \)
Proof
l0
cadan
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \vee \psi) \wedge (\varphi \vee \chi) \wedge (\psi \vee \chi) \)
3anass
\( \vdash (\varphi \vee \psi) \wedge (\varphi \vee \chi) \wedge (\psi \vee \chi) \leftrightarrow (\varphi \vee \psi) \wedge ((\varphi \vee \chi) \wedge (\psi \vee \chi)) \)
l2
bitri l0 _
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \vee \psi) \wedge ((\varphi \vee \chi) \wedge (\psi \vee \chi)) \)
l3
olc
olc
jca l3 _
biantrud _
\( \vdash \chi \rightarrow (\varphi \vee \psi \leftrightarrow (\varphi \vee \psi) \wedge ((\varphi \vee \chi) \wedge (\psi \vee \chi))) \)
bitr4id l2 _