Theorem hadifp 1634

Description: The value of the adder sum is, if the first input is true, the biconditionality, and if the first input is false, the exclusive disjunction, of the other two inputs. (Contributed by BJ, 11-Aug-2020.)

Assertion

Ref	Expression
hadifp	⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))

Proof of Theorem hadifp

Step	Hyp	Ref	Expression
1		had1 1632	. 2 ⊢ (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ↔ 𝜒)))
2		had0 1633	. 2 ⊢ (¬ 𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ⊻ 𝜒)))
3	1, 2	casesifp 1093	1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))

This proof depends on syntax axioms:   ↔ wb 209  if-wif 1077   ⊻ wxo 1540  haddwhad 1622

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-xor 1541  df-had 1623

This theorem is used by:  wl-df-3xor  38142