# Metamath Proof Explorer

## Theorem hadbi123d

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

Ref Expression
Hypotheses hadbid.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
hadbid.2 ${⊢}{\phi }\to \left({\theta }↔{\tau }\right)$
hadbid.3 ${⊢}{\phi }\to \left({\eta }↔{\zeta }\right)$
Assertion hadbi123d ${⊢}{\phi }\to \left(hadd\left({\psi },{\theta },{\eta }\right)↔hadd\left({\chi },{\tau },{\zeta }\right)\right)$

### Proof

Step Hyp Ref Expression
1 hadbid.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
2 hadbid.2 ${⊢}{\phi }\to \left({\theta }↔{\tau }\right)$
3 hadbid.3 ${⊢}{\phi }\to \left({\eta }↔{\zeta }\right)$
4 1 2 xorbi12d ${⊢}{\phi }\to \left(\left({\psi }⊻{\theta }\right)↔\left({\chi }⊻{\tau }\right)\right)$
5 4 3 xorbi12d ${⊢}{\phi }\to \left(\left(\left({\psi }⊻{\theta }\right)⊻{\eta }\right)↔\left(\left({\chi }⊻{\tau }\right)⊻{\zeta }\right)\right)$
6 df-had ${⊢}hadd\left({\psi },{\theta },{\eta }\right)↔\left(\left({\psi }⊻{\theta }\right)⊻{\eta }\right)$
7 df-had ${⊢}hadd\left({\chi },{\tau },{\zeta }\right)↔\left(\left({\chi }⊻{\tau }\right)⊻{\zeta }\right)$
8 5 6 7 3bitr4g ${⊢}{\phi }\to \left(hadd\left({\psi },{\theta },{\eta }\right)↔hadd\left({\chi },{\tau },{\zeta }\right)\right)$