Theorem cad0

If one input is false, then the adder carry is true exactly when both of the other two inputs are true. (Contributed by Mario Carneiro, 8-Sep-2016.) (Proof shortened by Wolf Lammen, 21-Sep-2024.)

Conclusion
\( \vdash \neg \chi \rightarrow (\text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi) \)
Proof
l0
df-cad
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \chi \wedge (\varphi \veebar \psi) \)
l1
idd
pm2.21
adantrd _
jaod l1 _
\( \vdash \neg \chi \rightarrow \varphi \wedge \psi \vee \chi \wedge (\varphi \veebar \psi) \rightarrow \varphi \wedge \psi \)
l5
biimtrid l0 _
cad11
impbid1 l5 _