Metamath Proof Explorer

Theorem wl-df2-3mintru2

Description: The adder carry in disjunctive normal form. An alternative highly symmetric definition emphasizing the independance of order of the inputs ph , ps and ch . Copy of cador . (Contributed by Mario Carneiro, 4-Sep-2016) df-cad redefined. (Revised by Wolf Lammen, 12-Jun-2024)

Ref Expression
Assertion wl-df2-3mintru2 ⊢ cadd φ ψ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 andi ⊢ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ φ ∧ χ
2 1 orbi1i ⊢ φ ∧ ψ ∨ χ ∨ ψ ∧ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ
3 wl-df-3mintru2 ⊢ cadd φ ψ χ ↔ if- φ ψ ∨ χ ψ ∧ χ
4 animorl ⊢ ψ ∧ χ → ψ ∨ χ
5 wl-ifpimpr ⊢ ψ ∧ χ → ψ ∨ χ → if- φ ψ ∨ χ ψ ∧ χ ↔ φ ∧ ψ ∨ χ ∨ ψ ∧ χ
6 4 5 ax-mp ⊢ if- φ ψ ∨ χ ψ ∧ χ ↔ φ ∧ ψ ∨ χ ∨ ψ ∧ χ
7 3 6 bitri ⊢ cadd φ ψ χ ↔ φ ∧ ψ ∨ χ ∨ ψ ∧ χ
8 df-3or ⊢ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ
9 2 7 8 3bitr4i ⊢ cadd φ ψ χ ↔ φ ∧ ψ ∨ φ ∧ χ ∨ ψ ∧ χ