Theorem cadifp

Description: The value of the carry is, if the input carry is true, the disjunction, and if the input carry is false, the conjunction, of the other two inputs. (Contributed by BJ, 8-Oct-2019)

	Ref	Expression
Assertion	cadifp	|- ( cadd ( ph , ps , ch ) <-> if- ( ch , ( ph \/ ps ) , ( ph /\ ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		cad1	|- ( ch -> ( cadd ( ph , ps , ch ) <-> ( ph \/ ps ) ) )
2		cad0	|- ( -. ch -> ( cadd ( ph , ps , ch ) <-> ( ph /\ ps ) ) )
3	1 2	casesifp	|- ( cadd ( ph , ps , ch ) <-> if- ( ch , ( ph \/ ps ) , ( ph /\ ps ) ) )