Metamath Proof Explorer


Theorem cad11

Description: If (at least) two inputs are true, then the adder carry is true. (Contributed by Mario Carneiro, 4-Sep-2016)

Ref Expression
Assertion cad11 φ ψ cadd φ ψ χ

Proof

Step Hyp Ref Expression
1 orc φ ψ φ ψ χ φ ψ
2 df-cad cadd φ ψ χ φ ψ χ φ ψ
3 1 2 sylibr φ ψ cadd φ ψ χ