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