Theorem cadbi123i

Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)

Hypotheses
cadbii.1
\( \vdash \varphi \leftrightarrow \psi \)
cadbii.2
\( \vdash \chi \leftrightarrow \theta \)
cadbii.3
\( \vdash \tau \leftrightarrow \eta \)
Conclusion
\( \vdash \text{ cadd } ( \varphi , \chi , \tau ) \leftrightarrow \text{ cadd } ( \psi , \theta , \eta ) \)
Proof
cadbii.1
l1
a1i _
cadbii.2
l3
a1i _
cadbii.3
a1i _
cadbi123d l1 l3 _
mptru _