Theorem cadifp 1557

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.)

Assertion

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

Proof of Theorem cadifp

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

Syntax hints:   <-> wb 196   \/ wo 383   /\ wa 384  if-wif 1012  caddwcad 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1013  df-3or 1038  df-3an 1039  df-xor 1465  df-cad 1546

This theorem is referenced by: (None)