Metamath Proof Explorer

Theorem cadan

Description: The adder carry in conjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 25-Sep-2018)

Ref Expression
Assertion cadan ⊢ cadd φ ψ χ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 df-3or ⊢ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ
2 cador ⊢ cadd φ ψ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ
3 andi ⊢ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ φ ∧ χ
4 3 orbi1i ⊢ φ ∧ ψ ∨ χ ∨ ψ ∧ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ
5 1 2 4 3bitr4i ⊢ cadd φ ψ χ ↔ φ ∧ ψ ∨ χ ∨ ψ ∧ χ
6 ordir ⊢ φ ∧ ψ ∨ χ ∨ ψ ∧ χ ↔ φ ∨ ψ ∧ χ ∧ ψ ∨ χ ∨ ψ ∧ χ
7 ordi ⊢ φ ∨ ψ ∧ χ ↔ φ ∨ ψ ∧ φ ∨ χ
8 orcom ⊢ ψ ∨ χ ∨ ψ ∧ χ ↔ ψ ∧ χ ∨ ψ ∨ χ
9 animorl ⊢ ψ ∧ χ → ψ ∨ χ
10 pm4.72 ⊢ ψ ∧ χ → ψ ∨ χ ↔ ψ ∨ χ ↔ ψ ∧ χ ∨ ψ ∨ χ
11 9 10 mpbi ⊢ ψ ∨ χ ↔ ψ ∧ χ ∨ ψ ∨ χ
12 8 11 bitr4i ⊢ ψ ∨ χ ∨ ψ ∧ χ ↔ ψ ∨ χ
13 7 12 anbi12i ⊢ φ ∨ ψ ∧ χ ∧ ψ ∨ χ ∨ ψ ∧ χ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ
14 5 6 13 3bitri ⊢ cadd φ ψ χ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ
15 df-3an ⊢ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ
16 14 15 bitr4i ⊢ cadd φ ψ χ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ