Theorem hadbi123d

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

	Ref	Expression
Hypotheses	hadbid.1	|- ( ph -> ( ps <-> ch ) )
	hadbid.2	|- ( ph -> ( th <-> ta ) )
	hadbid.3	|- ( ph -> ( et <-> ze ) )
Assertion	hadbi123d	|- ( ph -> ( hadd ( ps , th , et ) <-> hadd ( ch , ta , ze ) ) )

Proof

Step	Hyp	Ref	Expression
1		hadbid.1	|- ( ph -> ( ps <-> ch ) )
2		hadbid.2	|- ( ph -> ( th <-> ta ) )
3		hadbid.3	|- ( ph -> ( et <-> ze ) )
4	1 2	xorbi12d	|- ( ph -> ( ( ps \/_ th ) <-> ( ch \/_ ta ) ) )
5	4 3	xorbi12d	|- ( ph -> ( ( ( ps \/_ th ) \/_ et ) <-> ( ( ch \/_ ta ) \/_ ze ) ) )
6		df-had	|- ( hadd ( ps , th , et ) <-> ( ( ps \/_ th ) \/_ et ) )
7		df-had	|- ( hadd ( ch , ta , ze ) <-> ( ( ch \/_ ta ) \/_ ze ) )
8	5 6 7	3bitr4g	|- ( ph -> ( hadd ( ps , th , et ) <-> hadd ( ch , ta , ze ) ) )