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 ( ph , ps , ch ) <-> ( ( ph <-> ps ) <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		df-xor	|- ( ( ( ph \/_ ps ) \/_ ch ) <-> -. ( ( ph \/_ ps ) <-> ch ) )
2		df-had	|- ( hadd ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) )
3		xnor	|- ( ( ph <-> ps ) <-> -. ( ph \/_ ps ) )
4	3	bibi1i	|- ( ( ( ph <-> ps ) <-> ch ) <-> ( -. ( ph \/_ ps ) <-> ch ) )
5		nbbn	|- ( ( -. ( ph \/_ ps ) <-> ch ) <-> -. ( ( ph \/_ ps ) <-> ch ) )
6	4 5	bitri	|- ( ( ( ph <-> ps ) <-> ch ) <-> -. ( ( ph \/_ ps ) <-> ch ) )
7	1 2 6	3bitr4i	|- ( hadd ( ph , ps , ch ) <-> ( ( ph <-> ps ) <-> ch ) )