Metamath Proof Explorer

Theorem cadnot

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

Ref Expression
Assertion cadnot 
|- ( -. cadd ( ph , ps , ch ) <-> cadd ( -. ph , -. ps , -. ch ) )

Proof

Step Hyp Ref Expression
1 ianor 
 |-  ( -. ( ph /\ ps ) <-> ( -. ph \/ -. ps ) )
2 ianor 
 |-  ( -. ( ph /\ ch ) <-> ( -. ph \/ -. ch ) )
3 ianor 
 |-  ( -. ( ps /\ ch ) <-> ( -. ps \/ -. ch ) )
4 1 2 3 3anbi123i 
 |-  ( ( -. ( ph /\ ps ) /\ -. ( ph /\ ch ) /\ -. ( ps /\ ch ) ) <-> ( ( -. ph \/ -. ps ) /\ ( -. ph \/ -. ch ) /\ ( -. ps \/ -. ch ) ) )
5 3ioran 
 |-  ( -. ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) <-> ( -. ( ph /\ ps ) /\ -. ( ph /\ ch ) /\ -. ( ps /\ ch ) ) )
6 cador 
 |-  ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) )
7 5 6 xchnxbir 
 |-  ( -. cadd ( ph , ps , ch ) <-> ( -. ( ph /\ ps ) /\ -. ( ph /\ ch ) /\ -. ( ps /\ ch ) ) )
8 cadan 
 |-  ( cadd ( -. ph , -. ps , -. ch ) <-> ( ( -. ph \/ -. ps ) /\ ( -. ph \/ -. ch ) /\ ( -. ps \/ -. ch ) ) )
9 4 7 8 3bitr4i 
 |-  ( -. cadd ( ph , ps , ch ) <-> cadd ( -. ph , -. ps , -. ch ) )