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