Theorem cadifp 1651

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 1649	. 2 ⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓)))
2		cad0 1650	. 2 ⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓)))
3	1, 2	casesifp 1094	1 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861  if-wif 1078  caddwcad 1638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ifp 1079  df-3or 1104  df-3an 1105  df-xor 1541  df-cad 1639

This theorem is used by:  wl-df-3mintru2  38450