Metamath Proof Explorer

Theorem wl-df3-3mintru2

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

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

Proof

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