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