Metamath Proof Explorer


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 wff φ
1 wps wff ψ
2 wch wff χ
3 0 1 2 wcad wff cadd φ ψ χ
4 0 1 wa wff φ ψ
5 0 1 wxo wff φ ψ
6 2 5 wa wff χ φ ψ
7 4 6 wo wff φ ψ χ φ ψ
8 3 7 wb wff cadd φ ψ χ φ ψ χ φ ψ