Theorem hadbi

Description: The adder sum is the same as the triple biconditional. (Contributed by Mario Carneiro, 4-Sep-2016)

	Ref	Expression
Assertion	hadbi	⊢ ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ↔ 𝜓 ) ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		df-xor	⊢ ( ( ( 𝜑 ⊻ 𝜓 ) ⊻ 𝜒 ) ↔ ¬ ( ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) )
2		df-had	⊢ ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ⊻ 𝜓 ) ⊻ 𝜒 ) )
3		xnor	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( 𝜑 ⊻ 𝜓 ) )
4	3	bibi1i	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ↔ 𝜒 ) ↔ ( ¬ ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) )
5		nbbn	⊢ ( ( ¬ ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) ↔ ¬ ( ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) )
6	4 5	bitri	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ↔ 𝜒 ) ↔ ¬ ( ( 𝜑 ⊻ 𝜓 ) ↔ 𝜒 ) )
7	1 2 6	3bitr4i	⊢ ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ↔ 𝜓 ) ↔ 𝜒 ) )