hadbi123d

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

	Ref	Expression
Hypotheses	hadbid.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	hadbid.2	$⊢ φ \to (θ \leftrightarrow τ)$
	hadbid.3	$⊢ φ \to (η \leftrightarrow ζ)$
Assertion	hadbi123d	$⊢ φ \to (hadd (ψ, θ, η) \leftrightarrow hadd (χ, τ, ζ))$

Step	Hyp	Ref	Expression
1		hadbid.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		hadbid.2	$⊢ φ \to (θ \leftrightarrow τ)$
3		hadbid.3	$⊢ φ \to (η \leftrightarrow ζ)$
4	1 2	xorbi12d	$⊢ φ \to ((ψ ⊻ θ) \leftrightarrow (χ ⊻ τ))$
5	4 3	xorbi12d	$⊢ φ \to (((ψ ⊻ θ) ⊻ η) \leftrightarrow ((χ ⊻ τ) ⊻ ζ))$
6		df-had	$⊢ hadd (ψ, θ, η) \leftrightarrow ((ψ ⊻ θ) ⊻ η)$
7		df-had	$⊢ hadd (χ, τ, ζ) \leftrightarrow ((χ ⊻ τ) ⊻ ζ)$
8	5 6 7	3bitr4g	$⊢ φ \to (hadd (ψ, θ, η) \leftrightarrow hadd (χ, τ, ζ))$

Metamath Proof Explorer