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	$⊢ \neg χ \to (cadd (φ, ψ, χ) \leftrightarrow (φ \land ψ))$

Proof

Step	Hyp	Ref	Expression
1		df-cad	$⊢ cadd (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor (χ \land (φ ⊻ ψ)))$
2		idd	$⊢ \neg χ \to ((φ \land ψ) \to (φ \land ψ))$
3		pm2.21	$⊢ \neg χ \to (χ \to (φ \land ψ))$
4	3	adantrd	$⊢ \neg χ \to ((χ \land (φ ⊻ ψ)) \to (φ \land ψ))$
5	2 4	jaod	$⊢ \neg χ \to (((φ \land ψ) \lor (χ \land (φ ⊻ ψ))) \to (φ \land ψ))$
6	1 5	biimtrid	$⊢ \neg χ \to (cadd (φ, ψ, χ) \to (φ \land ψ))$
7		cad11	$⊢ (φ \land ψ) \to cadd (φ, ψ, χ)$
8	6 7	impbid1	$⊢ \neg χ \to (cadd (φ, ψ, χ) \leftrightarrow (φ \land ψ))$

Metamath Proof Explorer

Theorem cad0

Proof