Metamath Proof Explorer

Theorem cad0

Description: If one input is false, then the adder carry is true exactly when both of the other two inputs are true. (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Assertion cad0 ⊢ ¬ χ → cadd φ ψ χ ↔ φ ∧ ψ

Proof

Step Hyp Ref Expression
1 df-cad ⊢ cadd φ ψ χ ↔ φ ∧ ψ ∨ χ ∧ φ ⊻ ψ
2 idd ⊢ ¬ χ → φ ∧ ψ → φ ∧ ψ
3 pm2.21 ⊢ ¬ χ → χ → φ ∧ ψ
4 3 adantrd ⊢ ¬ χ → χ ∧ φ ⊻ ψ → φ ∧ ψ
5 2 4 jaod ⊢ ¬ χ → φ ∧ ψ ∨ χ ∧ φ ⊻ ψ → φ ∧ ψ
6 orc ⊢ φ ∧ ψ → φ ∧ ψ ∨ χ ∧ φ ⊻ ψ
7 5 6 impbid1 ⊢ ¬ χ → φ ∧ ψ ∨ χ ∧ φ ⊻ ψ ↔ φ ∧ ψ
8 1 7 syl5bb ⊢ ¬ χ → cadd φ ψ χ ↔ φ ∧ ψ