Definition df-cad

Description: Definition of the "carry" output of the full adder. It is true when at least two arguments are true, so it is equal to the "majority" function on three variables. See cador and cadan for alternate definitions. (Contributed by Mario Carneiro, 4-Sep-2016)

	Ref	Expression
Assertion	df-cad	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3	0 1 2	wcad	⊢ cadd ( 𝜑 , 𝜓 , 𝜒 )
4	0 1	wa	⊢ ( 𝜑 ∧ 𝜓 )
5	0 1	wxo	⊢ ( 𝜑 ⊻ 𝜓 )
6	2 5	wa	⊢ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) )
7	4 6	wo	⊢ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) )
8	3 7	wb	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ) )