Theorem hadbi123i

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

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