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φψχ↔φ∧ψ∨φ∧χ∨ψ∧χ