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