Theorem cad11

If (at least) two inputs are true, then the adder carry is true. (Contributed by Mario Carneiro, 4-Sep-2016.)

Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \text{ cadd } ( \varphi , \psi , \chi ) \)
Proof
l0
orc
\( \vdash \varphi \wedge \psi \rightarrow \varphi \wedge \psi \vee \chi \wedge (\varphi \veebar \psi) \)
df-cad
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \chi \wedge (\varphi \veebar \psi) \)
sylibr l0 _