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 ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ∧ 𝜓 ) ) ) |
| 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 ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ∧ 𝜓 ) ) ) |