Theorem cadifp 1648

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400   ∨ wo 860  if-wif 1077  caddwcad 1635

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 401  df-or 861  df-ifp 1078  df-3or 1103  df-3an 1104  df-xor 1541  df-cad 1636

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