Theorem hadnot

Description: The adder sum distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020)

	Ref	Expression
Assertion	hadnot	|- ( -. hadd ( ph , ps , ch ) <-> hadd ( -. ph , -. ps , -. ch ) )

Proof

Step	Hyp	Ref	Expression
1		notbi	|- ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) )
2	1	bibi1i	|- ( ( ( ph <-> ps ) <-> -. ch ) <-> ( ( -. ph <-> -. ps ) <-> -. ch ) )
3		xor3	|- ( -. ( ( ph <-> ps ) <-> ch ) <-> ( ( ph <-> ps ) <-> -. ch ) )
4		hadbi	|- ( hadd ( ph , ps , ch ) <-> ( ( ph <-> ps ) <-> ch ) )
5	3 4	xchnxbir	|- ( -. hadd ( ph , ps , ch ) <-> ( ( ph <-> ps ) <-> -. ch ) )
6		hadbi	|- ( hadd ( -. ph , -. ps , -. ch ) <-> ( ( -. ph <-> -. ps ) <-> -. ch ) )
7	2 5 6	3bitr4i	|- ( -. hadd ( ph , ps , ch ) <-> hadd ( -. ph , -. ps , -. ch ) )