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) (Proof shortened by Wolf Lammen, 21-Sep-2024)

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 1 5 biimtrid ⊢ ¬ χ → cadd φ ψ χ → φ ∧ ψ
7 cad11 ⊢ φ ∧ ψ → cadd φ ψ χ
8 6 7 impbid1 ⊢ ¬ χ → cadd φ ψ χ ↔ φ ∧ ψ