Metamath Proof Explorer

Theorem cad1

Description: If one input is true, then the adder carry is true exactly when at least one of the other two inputs is true. (Contributed by Mario Carneiro, 8-Sep-2016) (Proof shortened by Wolf Lammen, 19-Jun-2020)

Ref Expression
Assertion cad1 ⊢ χ → cadd φ ψ χ ↔ φ ∨ ψ

Proof

Step Hyp Ref Expression
1 cadan ⊢ cadd φ ψ χ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ
2 3anass ⊢ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ
3 1 2 bitri ⊢ cadd φ ψ χ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ
4 olc ⊢ χ → φ ∨ χ
5 olc ⊢ χ → ψ ∨ χ
6 4 5 jca ⊢ χ → φ ∨ χ ∧ ψ ∨ χ
7 6 biantrud ⊢ χ → φ ∨ ψ ↔ φ ∨ ψ ∧ φ ∨ χ ∧ ψ ∨ χ
8 3 7 bitr4id ⊢ χ → cadd φ ψ χ ↔ φ ∨ ψ