Theorem cadifp 1621

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(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓)))

Proof of Theorem cadifp

Step	Hyp	Ref	Expression
1		cad1 1619	. 2 ⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓)))
2		cad0 1620	. 2 ⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓)))
3	1, 2	casesifp 1078	1 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 848  if-wif 1063  caddwcad 1608

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 207  df-an 396  df-or 849  df-ifp 1064  df-3or 1088  df-3an 1089  df-xor 1514  df-cad 1609

This theorem is referenced by:  wl-df-3mintru2  37736