Metamath Proof Explorer

Theorem wl-df4-3mintru2

Description: An alternative definition of the adder carry. Copy of df-cad . (Contributed by Mario Carneiro, 4-Sep-2016) df-cad redefined. (Revised by Wolf Lammen, 19-Jun-2024)

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

Proof

Step Hyp Ref Expression
1 3orass ⊢φ∧ψ∨φ∧χ∨ψ∧χ↔φ∧ψ∨φ∧χ∨ψ∧χ
2 wl-df2-3mintru2 ⊢caddφψχ↔φ∧ψ∨φ∧χ∨ψ∧χ
3 xor2 ⊢φ⊻ψ↔φ∨ψ∧¬φ∧ψ
4 3 biancomi ⊢φ⊻ψ↔¬φ∧ψ∧φ∨ψ
5 4 anbi1ci ⊢χ∧φ⊻ψ↔¬φ∧ψ∧φ∨ψ∧χ
6 anass ⊢¬φ∧ψ∧φ∨ψ∧χ↔¬φ∧ψ∧φ∨ψ∧χ
7 5 6 bitri ⊢χ∧φ⊻ψ↔¬φ∧ψ∧φ∨ψ∧χ
8 7 orbi2i ⊢φ∧ψ∨χ∧φ⊻ψ↔φ∧ψ∨¬φ∧ψ∧φ∨ψ∧χ
9 pm5.63 ⊢φ∧ψ∨φ∨ψ∧χ↔φ∧ψ∨¬φ∧ψ∧φ∨ψ∧χ
10 andir ⊢φ∨ψ∧χ↔φ∧χ∨ψ∧χ
11 10 orbi2i ⊢φ∧ψ∨φ∨ψ∧χ↔φ∧ψ∨φ∧χ∨ψ∧χ
12 8 9 11 3bitr2i ⊢φ∧ψ∨χ∧φ⊻ψ↔φ∧ψ∨φ∧χ∨ψ∧χ
13 1 2 12 3bitr4i ⊢caddφψχ↔φ∧ψ∨χ∧φ⊻ψ