Theorem cadtru

The adder carry is true as soon as its first two inputs are the truth constant. (Contributed by Mario Carneiro, 4-Sep-2016.)

Conclusion
\( \vdash \text{ cadd } ( \top , \top , \varphi ) \)
Proof
l0
tru
\( \vdash \top \)
l1
tru
\( \vdash \top \)
cad11
\( \vdash \top \wedge \top \rightarrow \text{ cadd } ( \top , \top , \varphi ) \)
mp2an l0 l1 _