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	|- ( ( ph /\ ps ) -> cadd ( ph , ps , ch ) )

Proof

Step	Hyp	Ref	Expression
1		orc	|- ( ( ph /\ ps ) -> ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) )
2		df-cad	|- ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) )
3	1 2	sylibr	|- ( ( ph /\ ps ) -> cadd ( ph , ps , ch ) )