Metamath Proof Explorer

Theorem cador

Description: The adder carry in disjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 xor2 ⊢ φ ⊻ ψ ↔ φ ∨ ψ ∧ ¬ φ ∧ ψ
2 1 rbaib ⊢ ¬ φ ∧ ψ → φ ⊻ ψ ↔ φ ∨ ψ
3 2 anbi1d ⊢ ¬ φ ∧ ψ → φ ⊻ ψ ∧ χ ↔ φ ∨ ψ ∧ χ
4 ancom ⊢ φ ⊻ ψ ∧ χ ↔ χ ∧ φ ⊻ ψ
5 andir ⊢ φ ∨ ψ ∧ χ ↔ φ ∧ χ ∨ ψ ∧ χ
6 3 4 5 3bitr3g ⊢ ¬ φ ∧ ψ → χ ∧ φ ⊻ ψ ↔ φ ∧ χ ∨ ψ ∧ χ
7 6 pm5.74i ⊢ ¬ φ ∧ ψ → χ ∧ φ ⊻ ψ ↔ ¬ φ ∧ ψ → φ ∧ χ ∨ ψ ∧ χ
8 df-or ⊢ φ ∧ ψ ∨ χ ∧ φ ⊻ ψ ↔ ¬ φ ∧ ψ → χ ∧ φ ⊻ ψ
9 df-or ⊢ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ ↔ ¬ φ ∧ ψ → φ ∧ χ ∨ ψ ∧ χ
10 7 8 9 3bitr4i ⊢ φ ∧ ψ ∨ χ ∧ φ ⊻ ψ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ
11 df-cad ⊢ cadd φ ψ χ ↔ φ ∧ ψ ∨ χ ∧ φ ⊻ ψ
12 3orass ⊢ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ
13 10 11 12 3bitr4i ⊢ cadd φ ψ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ