# Metamath Proof Explorer

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\left({\phi },{\psi },{\chi }\right)↔cadd\left(¬{\phi },¬{\psi },¬{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 ianor ${⊢}¬\left({\phi }\wedge {\psi }\right)↔\left(¬{\phi }\vee ¬{\psi }\right)$
2 ianor ${⊢}¬\left({\phi }\wedge {\chi }\right)↔\left(¬{\phi }\vee ¬{\chi }\right)$
3 ianor ${⊢}¬\left({\psi }\wedge {\chi }\right)↔\left(¬{\psi }\vee ¬{\chi }\right)$
4 1 2 3 3anbi123i ${⊢}\left(¬\left({\phi }\wedge {\psi }\right)\wedge ¬\left({\phi }\wedge {\chi }\right)\wedge ¬\left({\psi }\wedge {\chi }\right)\right)↔\left(\left(¬{\phi }\vee ¬{\psi }\right)\wedge \left(¬{\phi }\vee ¬{\chi }\right)\wedge \left(¬{\psi }\vee ¬{\chi }\right)\right)$
5 3ioran ${⊢}¬\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge {\chi }\right)\vee \left({\psi }\wedge {\chi }\right)\right)↔\left(¬\left({\phi }\wedge {\psi }\right)\wedge ¬\left({\phi }\wedge {\chi }\right)\wedge ¬\left({\psi }\wedge {\chi }\right)\right)$
6 cador ${⊢}cadd\left({\phi },{\psi },{\chi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge {\chi }\right)\vee \left({\psi }\wedge {\chi }\right)\right)$
7 5 6 xchnxbir ${⊢}¬cadd\left({\phi },{\psi },{\chi }\right)↔\left(¬\left({\phi }\wedge {\psi }\right)\wedge ¬\left({\phi }\wedge {\chi }\right)\wedge ¬\left({\psi }\wedge {\chi }\right)\right)$
8 cadan ${⊢}cadd\left(¬{\phi },¬{\psi },¬{\chi }\right)↔\left(\left(¬{\phi }\vee ¬{\psi }\right)\wedge \left(¬{\phi }\vee ¬{\chi }\right)\wedge \left(¬{\psi }\vee ¬{\chi }\right)\right)$
9 4 7 8 3bitr4i ${⊢}¬cadd\left({\phi },{\psi },{\chi }\right)↔cadd\left(¬{\phi },¬{\psi },¬{\chi }\right)$